∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R),
  MvPolynomial.coeff m (p * (MvPolynomial.monomial s) r) = if s ≤ m then MvPolynomial.coeff (m - s) p * r else 0