[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
⊢ ↑(choose b a) = ↑b ! / (↑a ! * ↑(b - a)!)
[PROOFSTEP]
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_ne_zero _)
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(choose b a) = ↑b ! / (↑a ! * ↑(b - a)!)
[PROOFSTEP]
rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
this : ∀ {n : ℕ}, ↑n ! ≠ 0
⊢ ↑(choose b a) * (↑a ! * ↑(b - a)!) = ↑b !
[PROOFSTEP]
rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(choose (a + b) a) = ↑(a + b)! / (↑a ! * ↑b !)
[PROOFSTEP]
rw [cast_choose K (_root_.le_add_right le_rfl), add_tsub_cancel_left]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
⊢ ↑(choose a b) = Polynomial.eval (↑(a - (b - 1))) (pochhammer K b) / ↑b !
[PROOFSTEP]
rw [eq_div_iff_mul_eq (cast_ne_zero.2 b.factorial_ne_zero : (b ! : K) ≠ 0), ← cast_mul, mul_comm, ←
  descFactorial_eq_factorial_mul_choose, ← cast_descFactorial]
[GOAL]
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a : ℕ
⊢ ↑(choose a 2) = ↑a * (↑a - 1) / 2
[PROOFSTEP]
rw [← cast_descFactorial_two, descFactorial_eq_factorial_mul_choose, factorial_two, mul_comm, cast_mul, cast_two,
  eq_div_iff_mul_eq (two_ne_zero : (2 : K) ≠ 0)]
