C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 - (0 - a) = a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ - -a = a
rw [neg_def, neg_def]
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - a - (0 - a) = a
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ 0 - (0 - a) = a
conv_lhs =>
  congr; rw [← sub_self a]
no goals
C : Type u
inst✝¹ : Category C
inst✝ : NonPreadditiveAbelian C
X Y : C
a : X ⟶ Y
⊢ a - a - (0 - a) = a
rw [sub_sub_sub, sub_zero, sub_self, sub_zero]