let n be Nat; :: thesis: for a being non trivial Nat
for b being non zero Nat st b < a |^ n holds
a |-count b < n
let a be non trivial Nat; :: thesis: for b being non zero Nat st b < a |^ n holds
a |-count b < n
let b be non zero Nat; :: thesis: ( b < a |^ n implies a |-count b < n )
assume b < a |^ n ; :: thesis: a |-count b < n
then ( 1 * (a |^ 0) divides b & not a |^ (0 + n) divides b ) by INT_2:12, NAT_D:7;
hence a |-count b < n by Count1; :: thesis: verum