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 σ
p q : MvPolynomial σ R
⊢ degrees (p - q) ≤ degrees p ⊔ degrees q
simpa only [sub_eq_add_neg] using le_trans (degrees_add p (-q)) (by rw [degrees_neg])
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 σ
p q : MvPolynomial σ R
⊢ degrees p ⊔ degrees (-q) ≤ degrees p ⊔ degrees q
rw [degrees_neg]