rw [sub_eq_add_neg, ofFinsupp_add, ofFinsupp_neg]
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := a - b } = { toFinsupp := a } - { toFinsupp := b }
R : Type u
a✝ b✝ : R
m n : ℕ
inst✝¹ : Semiring R
φ✝ : R →+* R
p q : R[X;φ✝]
S : Type u
inst✝ : Ring S
φ : S →+* S
a b : AddMonoidAlgebra S ℕ
⊢ { toFinsupp := a } + -{ toFinsupp := b } = { toFinsupp := a } - { toFinsupp := b }