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) [DivisionRing K] [CharZero K] {a : ℕ} {b : ℕ} (h : a ≤ b) : ↑(Nat.choose b a) = ↑(Nat.factorial b) / (↑(Nat.factorial a) * ↑(Nat.factorial (b - a)))

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

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

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