let a be non trivial Nat; for b, n being non zero Nat st b < a holds
a |-count (b |^ n) < n
let b, n be non zero Nat; ( b < a implies a |-count (b |^ n) < n )
assume A1:
b < a
; a |-count (b |^ n) < n
b >= 0 + 1
by NAT_1:13;
then A2:
a |-count b = 0
by A1, NAT_3:23;
a |-count (b |^ n) < n * ((a |-count b) + 1)
by Count2;
hence
a |-count (b |^ n) < n
by A2; verum