no goals
α : Type u
β : Type v
X : Type ?u.197176
ι : Type ?u.197179
inst✝ : PseudoMetricSpace α
x y : ℝ
hx : x ∈ Icc 0 1
hy : y ∈ Icc 0 1
⊢ dist x y ≤ 1
simpa only [sub_zero] using Real.dist_le_of_mem_Icc hx hy