theorem :: NEWTON02:124

for b being Nat holds b ! <= b |^ b