rw [totalDegree, Finset.sup_lt_iff]
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
case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ∀ b ∈ (∑ v ∈ p.support \ p.leadingTerms.support, (monomial v) (coeff v p)).support,
    (b.sum fun x e => e) < p.totalDegree

case right
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p : MvPolynomial ι R
hp : p.totalDegree ≠ 0
this : DecidableEq ι := Classical.decEq ι
⊢ ⊥ < p.totalDegree