no goals
R : Type u
S : Type v
σ : Type u_1
a a' a₁ a₂ : R
e : ℕ
n m : σ
s : σ →₀ ℕ
inst✝¹ : CommRing R
p q : MvPolynomial σ R
inst✝ : DecidableEq σ
⊢ vars (p - q) ⊆ vars p ∪ vars q
convert vars_add_subset p (-q) using 2 <;> simp [sub_eq_add_neg]