Nat.cast_descFactorial_two

theorem Nat.cast_descFactorial_two : ∀ (S : Type u_1) [inst : Ring S] (a : ℕ), ↑(a.descFactorial 2) = ↑a * (↑a - 1)

This theorem, `Nat.cast_descFactorial_two`, states that for any natural number `a` and for any Ring structure `S`, the descending factorial of `a` with `2` (denoted as `a.descFactorial 2`) when cast to the Ring structure `S`, is equal to `a` times `a - 1` in structure `S`. The subtraction in `a - 1` is not truncated subtraction, unlike the definition of `Nat.descFactorial`.

More concisely: For any natural number `a` and Ring `S`, `a.descFactorial 2` in `S` equals `a * (a - 1)` in `S`.