Commit 2022-12-16 12:16 740c2555

View on Github →

feat: Port Data.Nat.Factorial.Basic (#1066) d012cd09a9b256d870751284dd6a29882b0be105

Estimated changes

added def Nat.ascFactorial
added theorem Nat.ascFactorial_pos
added theorem Nat.ascFactorial_succ
added theorem Nat.ascFactorial_zero
added theorem Nat.descFactorial_one
added theorem Nat.descFactorial_self
added theorem Nat.descFactorial_succ
added theorem Nat.descFactorial_zero
added theorem Nat.dvd_factorial
added def Nat.factorial
added theorem Nat.factorial_eq_one
added theorem Nat.factorial_inj
added theorem Nat.factorial_le
added theorem Nat.factorial_lt
added theorem Nat.factorial_ne_zero
added theorem Nat.factorial_one
added theorem Nat.factorial_pos
added theorem Nat.factorial_succ
added theorem Nat.factorial_two
added theorem Nat.factorial_zero
added theorem Nat.lt_factorial_self
added theorem Nat.monotone_factorial
added theorem Nat.mul_factorial_pred
added theorem Nat.one_lt_factorial
added theorem Nat.self_le_factorial
added theorem Nat.succ_ascFactorial
added theorem Nat.succ_descFactorial
added theorem Nat.zero_ascFactorial