no goals
ι : Type ?u.89441
α : Type u_1
β : Type ?u.89447
inst✝ : LinearOrderedSemifield α
a✝ b c d e : α
m n : ℤ
a : α
⊢ a / 2 + a / 2 = a
rw [div_add_div_same, ← two_mul, mul_div_cancel_left a two_ne_zero]