no goals
𝕜 : Type ?u.76649
E : Type u_1
inst✝⁴ : NormedLinearOrderedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace ℝ E
inst✝ : StrictConvexSpace ℝ E
x y z : E
a b r : ℝ
⊢ dist x y + dist y z = dist x z ↔ y ∈ [x-[ℝ]z]
simp only [mem_segment_iff_sameRay, sameRay_iff_norm_add, dist_eq_norm', sub_add_sub_cancel',
  eq_comm]