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