no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : CommRing R
n k : ℕ
c : R
⊢ (↑derivative^[k]) ((X - ↑C c) ^ n) = ↑(∏ i in range k, (n - i)) * (X - ↑C c) ^ (n - k)
rw [sub_eq_add_neg, ← C_neg, iterate_derivative_X_add_pow]