theorem :: NEWTON03:61

for a being non trivial Nat
for b, n being non zero Nat st b < a holds
a |-count (b |^ n) < n