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) [Semiring S] (a : ℕ) (b : ℕ) : ↑(Nat.ascFactorial a b) = Polynomial.eval (↑a) (ascPochhammer S b)

theorem Nat.cast_descFactorial (S : Type u_1) [Semiring S] (a : ℕ) (b : ℕ) : ↑(Nat.descFactorial a b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer S b)

theorem Nat.cast_factorial (S : Type u_1) [Semiring S] (a : ℕ) : ↑(Nat.factorial a) = Polynomial.eval 1 (ascPochhammer S a)

theorem Nat.cast_descFactorial_two (S : Type u_1) [Ring S] (a : ℕ) : ↑(Nat.descFactorial a 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.