let a be non trivial Nat; :: thesis: for b being non zero Nat holds a |^ (a |-count b) <= b
let b be non zero Nat; :: thesis: a |^ (a |-count b) <= b
a <> 1 by Def0;
then a |^ (a |-count b) divides b by NAT_3:def 7;
hence a |^ (a |-count b) <= b by NAT_D:7; :: thesis: verum