Metric.eannulusIcc_ofReal

lemma eannulusIcc_ofReal (h : 0 < r ∨ 0 ≤ R) :    eannulusIcc x (ENNReal.ofReal r) (ENNReal.ofReal R) = annulusIcc x r R := by  by_cases hR : 0 ≤ R  · ext y    simp [eannulusIcc, annulusIcc, edist_dist, mem_Icc,      ENNReal.ofReal_le_ofReal_iff dist_nonneg,      ENNReal.ofReal_le_ofReal_iff hR]  · have hr : 0 < r := h.resolve_right hR    have hR' : R < 0 := lt_of_not_ge hR    have hRr : R < r := hR'.trans hr    have hER : ENNReal.ofReal R < ENNReal.ofReal r :=      (ENNReal.ofReal_lt_ofReal_iff').2 ⟨hRr, hr⟩    -- both sides are empty, since the corresponding intervals are empty    simp [annulusIcc, Icc_eq_empty_of_lt hRr, eannulusIcc, Icc_eq_empty_of_lt hER]