have : support (C r * p) = p.support := by
  rw [C_mul']
  exact Finsupp.support_smul_eq hr
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
⊢ (C r * p).leadingTerms = C r * p.leadingTerms
case neg
R : Type u_1
ι : Type u_2
inst✝¹ : CommSemiring R
inst✝ : NoZeroSMulDivisors R R
p : MvPolynomial ι R
r : R
hr : ¬r = 0
this : (C r * p).support = p.support
⊢ (C r * p).leadingTerms = C r * p.leadingTerms