# 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.

source
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.