theorem :: NUMERAL3:63

for a, b being non trivial Nat ex n being Nat st
( b |^ n <= a & a < b |^ (n + 1) )