have := congr_arg support hp
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
⊢ p = 0
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
h : Disjoint p.support q.support
hp : p + q = 0
this : (p + q).support = support 0
⊢ p = 0