ι : Type ?u.183426
α : Type u_1
β : Type ?u.183432
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 + a / 2 - a / 2 = a / 2
ι : Type ?u.183426
α : Type u_1
β : Type ?u.183432
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a - a / 2 = a / 2
suffices a / 2 + a / 2 - a / 2 = a / 2 by rwa [add_halves] at this
no goals
ι : Type ?u.183426
α : Type u_1
β : Type ?u.183432
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
⊢ a / 2 + a / 2 - a / 2 = a / 2
rw [add_sub_cancel]
no goals
ι : Type ?u.183426
α : Type u_1
β : Type ?u.183432
inst✝ : LinearOrderedField α
a✝ b c d : α
n : ℤ
a : α
this : a / 2 + a / 2 - a / 2 = a / 2
⊢ a - a / 2 = a / 2
rwa [add_halves] at this