no goals
R : Type u
S : Type v
T : Type w
ι : Type y
A : Type z
a b : R
n✝ : ℕ
inst✝ : Semiring R
p : R[X]
n : ℕ
h : n ∈ support (↑derivative p)
h1 : coeff p (n + 1) = 0
⊢ coeff (↑derivative p) n = 0
rw [coeff_derivative, h1, zero_mul]