no goals
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a : ℕ
⊢ ↑(choose a 2) = ↑a * (↑a - 1) / 2
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)]