Cast of binomial coefficients

This file allows calculating the binomial coefficient a.choose b as an element of a division ring of characteristic 0.

theorem Nat.cast_choose (K : Type u_1) [DivisionSemiring K] [CharZero K] {a b : ℕ} (h : a ≤ b) : ↑(b.choose a) = ↑b.factorial / (↑a.factorial * ↑(b - a).factorial)

theorem Nat.cast_add_choose (K : Type u_1) [DivisionSemiring K] [CharZero K] {a b : ℕ} : ↑((a + b).choose a) = ↑(a + b).factorial / (↑a.factorial * ↑b.factorial)

theorem Nat.cast_choose_eq_ascPochhammer_div (K : Type u_1) [DivisionSemiring K] [CharZero K] (a b : ℕ) : ↑(a.choose b) = Polynomial.eval (↑(a - (b - 1))) (ascPochhammer K b) / ↑b.factorial

theorem Nat.cast_choose_eq_descPochhammer_div (K : Type u_1) [DivisionRing K] [CharZero K] (a b : ℕ) : ↑(a.choose b) = Polynomial.eval (↑a) (descPochhammer K b) / ↑b.factorial

theorem Nat.cast_choose_two (K : Type u_1) [DivisionRing K] [CharZero K] (a : ℕ) : ↑(a.choose 2) = ↑a * (↑a - 1) / 2