no goals
R : Type u
S : Type v
T : Type w
A : Type z
a b : R
n : ℕ
inst✝ : Semiring R
p✝ q p : R[X]
⊢ ∀ (n : ℕ), coeff (divX p * X + ↑C (coeff p 0)) n = coeff p n
rintro ⟨_ | _⟩ <;> simp [coeff_C, Nat.succ_ne_zero, coeff_mul_X]