Theorem Nat.factorial_lt

Modification history