intro m hm
case mpr.h.a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
⊢ ∀ b ∈ p.support, b i ≤ 0
case mpr.h.a
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
i : ι
p : MvPolynomial ι R
h : ∀ j ∈ p.support, j i = 0
m : ι →₀ ℕ
hm : m ∈ p.support
⊢ m i ≤ 0