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)!)
K : Type u_1
inst✝¹ : DivisionRing K
inst✝ : CharZero K
a b : ℕ
h : a ≤ b
⊢ ↑(choose b a) = ↑b ! / (↑a ! * ↑(b - a)!)
have : ∀ {n : ℕ}, (n ! : K) ≠ 0 := Nat.cast_ne_zero.2 (factorial_ne_zero _)
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 !
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)!)
rw [eq_div_iff_mul_eq (mul_ne_zero this this)]
no goals
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 !
rw_mod_cast [← mul_assoc, choose_mul_factorial_mul_factorial h]