α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -a + -(n • x) = -(n • x) + -a
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -termg n x a = termg n' x a'
simp [h₂.symm, h₁.symm, termg]
no goals
α : Type u_1
inst✝ : AddCommGroup α
n : ℤ
x a : α
n' : ℤ
a' : α
h₁ : -n = n'
h₂ : -a = a'
⊢ -a + -(n • x) = -(n • x) + -a
exact add_comm _ _