[GOAL]
α : Type u_1
a b a' b' : α
inst✝ : AddGroup α
p : a = b
H : a' - b' - (a - b) = 0
⊢ a' = b'
[PROOFSTEP]
rw [← sub_eq_zero] at p ⊢
[GOAL]
α : Type u_1
a b a' b' : α
inst✝ : AddGroup α
p✝ : a = b
p : a - b = 0
H : a' - b' - (a - b) = 0
⊢ a' - b' = 0
[PROOFSTEP]
rwa [sub_eq_zero, p] at H 
