no goals
α : Type ?u.807039
β : Type ?u.807042
a b c d : ℝ≥0∞
r p✝ q✝ : ℝ≥0
p q : ℝ
hp : 0 ≤ p
⊢ ENNReal.ofReal p < ENNReal.ofReal q ↔ p < q
rw [ENNReal.ofReal, ENNReal.ofReal, coe_lt_coe, Real.toNNReal_lt_toNNReal_iff_of_nonneg hp]