no goals
α : Type u
β : Type v
X : Type ?u.196294
ι : Type ?u.196297
inst✝ : PseudoMetricSpace α
x y x' y' : ℝ
hx : x ∈ Icc x' y'
hy : y ∈ Icc x' y'
⊢ dist x y ≤ y' - x'
simpa only [Real.dist_eq, abs_of_nonpos (sub_nonpos.2 <| hx.1.trans hx.2), neg_sub] using
  Real.dist_le_of_mem_uIcc (Icc_subset_uIcc hx) (Icc_subset_uIcc hy)