# Cast of factorials #

This file allows calculating factorials (including ascending and descending ones) as elements of a semiring.

This is particularly crucial for Nat.descFactorial as subtraction on does not correspond to subtraction on a general semiring. For example, we can't rely on existing cast lemmas to prove ↑(a.descFactorial 2) = ↑a * (↑a - 1). We must use the fact that, whenever ↑(a - 1) is not equal to ↑a - 1, the other factor is 0 anyway.

theorem Nat.cast_ascFactorial (S : Type u_1) [] (a : ) (b : ) :
(a.ascFactorial b) = Polynomial.eval (a) ()
theorem Nat.cast_descFactorial (S : Type u_1) [] (a : ) (b : ) :
(a.descFactorial b) = Polynomial.eval ((a - (b - 1))) ()
theorem Nat.cast_factorial (S : Type u_1) [] (a : ) :
a.factorial = Polynomial.eval 1 ()
theorem Nat.cast_descFactorial_two (S : Type u_1) [Ring S] (a : ) :
(a.descFactorial 2) = a * (a - 1)

Convenience lemma. The a - 1 is not using truncated subtraction, as opposed to the definition of Nat.descFactorial as a natural.