Lemmas about distances between points in intervals in ℝ.

theorem Real.dist_left_le_of_mem_uIcc {x : ℝ} {y : ℝ} {z : ℝ} (h : y ∈ Set.uIcc x z) : dist x y ≤ dist x z

theorem Real.dist_right_le_of_mem_uIcc {x : ℝ} {y : ℝ} {z : ℝ} (h : y ∈ Set.uIcc x z) : dist y z ≤ dist x z

theorem Real.dist_le_of_mem_uIcc {x : ℝ} {y : ℝ} {x' : ℝ} {y' : ℝ} (hx : x ∈ Set.uIcc x' y') (hy : y ∈ Set.uIcc x' y') : dist x y ≤ dist x' y'

theorem Real.dist_le_of_mem_Icc {x : ℝ} {y : ℝ} {x' : ℝ} {y' : ℝ} (hx : x ∈ Set.Icc x' y') (hy : y ∈ Set.Icc x' y') : dist x y ≤ y' - x'

theorem Real.dist_le_of_mem_Icc_01 {x : ℝ} {y : ℝ} (hx : x ∈ Set.Icc 0 1) (hy : y ∈ Set.Icc 0 1) : dist x y ≤ 1

theorem Real.dist_le_of_mem_pi_Icc {ι : Type u_1} [Fintype ι] {x : ι → ℝ} {y : ι → ℝ} {x' : ι → ℝ} {y' : ι → ℝ} (hx : x ∈ Set.Icc x' y') (hy : y ∈ Set.Icc x' y') : dist x y ≤ dist x' y'