constructor
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p) ∧
    (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).totalDegree < p.totalDegree
case left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ p = p.leadingTerms + ∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)

case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).totalDegree < p.totalDegree