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 σ
hpq : Disjoint (vars p) (vars (-q))
⊢ vars (p - q) = vars p ∪ vars q
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 σ
hpq : Disjoint (vars p) (vars q)
⊢ vars (p - q) = vars p ∪ vars q
rw [← vars_neg q] at hpq
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 σ
hpq : Disjoint (vars p) (vars (-q))
⊢ vars (p - q) = vars p ∪ vars q
convert vars_add_of_disjoint hpq using 2 <;> simp [sub_eq_add_neg]