ι : Type ?u.184413
α : Type u_1
β : Type ?u.184419
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 - (a / 2 + a / 2) = -(a / 2)
ι : Type ?u.184413
α : Type u_1
β : Type ?u.184419
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 - a = -(a / 2)
suffices a / 2 - (a / 2 + a / 2) = -(a / 2) by rwa [add_halves] at this
no goals
ι : Type ?u.184413
α : Type u_1
β : Type ?u.184419
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 - (a / 2 + a / 2) = -(a / 2)
rw [sub_add_eq_sub_sub, sub_self, zero_sub]
no goals
ι : Type ?u.184413
α : Type u_1
β : Type ?u.184419
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
this : a / 2 - (a / 2 + a / 2) = -(a / 2)
⊢ a / 2 - a = -(a / 2)
rwa [add_halves] at this