no goals
R : Type u
S : Type v
ι : Type w
a b : R
m n : ℕ
inst✝ : Semiring R
p q r f g : R[X]
⊢ coeff (f * g) (natDegree f + natDegree g) = coeff f (natDegree f) * coeff g (natDegree g)
simp only [coeff_natDegree, coeff_mul_degree_add_degree]