no goals
α : Type u
β : Type v
X : Type ?u.194701
ι : Type ?u.194704
inst✝ : PseudoMetricSpace α
x y z : ℝ
h : y ∈ uIcc x z
⊢ dist x y ≤ dist x z
simpa only [dist_comm x] using abs_sub_left_of_mem_uIcc h