for b being Nat holds
( b > 1 iff b ! > 1 )