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