classical
contrapose! hp
have := congr_arg support hp
rw [support_zero, support_add_eq h,
  Finset.union_eq_empty,MvPolynomial.support_eq_empty] at this
exact this.left
R : Type u_1
ι : Type u_2
inst✝ : CommSemiring R
p q : MvPolynomial ι R
hp : p ≠ 0
h : Disjoint p.support q.support
⊢ p + q ≠ 0
no goals