no goals
α : Type ?u.806824
β : Type ?u.806827
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
h : 0 < q
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff h]