no goals
α : Type ?u.561104
β : Type ?u.561107
γ : Type ?u.561110
inst✝ : PseudoEMetricSpace α
a b : ℝ
h : a ≤ b
⊢ Metric.diam (Icc a b) = b - a
simp [Metric.diam, ENNReal.toReal_ofReal (sub_nonneg.2 h)]