no goals
R : Type u
a b : R
m✝ n✝ : ℕ
inst✝ : Semiring R
p q : R[X]
n m : ℕ
r s : R
⊢ (↑(monomial n) r * ↑(monomial m) s).toFinsupp = (↑(monomial (n + m)) (r * s)).toFinsupp
simp only [toFinsupp_monomial, toFinsupp_mul, AddMonoidAlgebra.single_mul_single]