Commit 2023-11-17 11:02 e7f5d814

View on Github →

fix: some cleanup in Nat.Factorial.Basic (#8422)

  • Also remove some unimportant porting notes in Order.Concept.

Estimated changes

modified theorem Nat.ascFactorial_succ
modified theorem Nat.descFactorial_one
modified theorem Nat.descFactorial_succ
added theorem Nat.factorial_inj'
modified theorem Nat.factorial_inj
deleted theorem Nat.factorial_le_of_le
modified theorem Nat.factorial_one
modified theorem Nat.factorial_succ
modified theorem Nat.factorial_two
modified theorem Nat.factorial_zero
modified theorem Nat.zero_descFactorial_succ