no goals
α : Type u_1
β : Type ?u.2661
γ : Type ?u.2664
inst✝ : BooleanRing α
a b : α
⊢ -a = -a + 0
rw [add_zero]
no goals
α : Type u_1
β : Type ?u.2661
γ : Type ?u.2664
inst✝ : BooleanRing α
a b : α
⊢ -a + 0 = -a + -a + a
rw [← neg_add_self, add_assoc]
no goals
α : Type u_1
β : Type ?u.2661
γ : Type ?u.2664
inst✝ : BooleanRing α
a b : α
⊢ -a + -a + a = a
rw [add_self, zero_add]