no goals
α : Type ?u.800710
β : Type ?u.800713
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
h : ENNReal.toNNReal a < ENNReal.toNNReal b
⊢ a < b
rwa [← coe_toNNReal ha, ← coe_toNNReal hb, coe_lt_coe]