for l being Nat holds l ! >= l