no goals
α : Type u
β : Type v
X : Type ?u.201326
ι : Type ?u.201329
inst✝ : PseudoMetricSpace α
x y : ℝ
⊢ Icc x y = closedBall ((x + y) / 2) ((y - x) / 2)
rw [Real.closedBall_eq_Icc, ← sub_div, add_comm, ← sub_add, add_sub_cancel', add_self_div_two, ←
  add_div, add_assoc, add_sub_cancel'_right, add_self_div_two]