Theorem Nat.factorial_dvd_ascFactorial

Modification history