Theorem: Real.closedBall_eq_segment (LeanCamCombi/ConvexContinuous.lean)

State before:
ε r : ℝ
hε : 0 ≤ ε
⊢ closedBall r ε = segment ℝ (r - ε) (r + ε)
Tactic:
rw [closedBall_eq_Icc, segment_eq_Icc ((sub_le_self _ hε).trans $ le_add_of_nonneg_right hε)]
State after:
no goals