Theorem Nat.add_factorial_succ_lt_factorial_add_succ

Modification history