no goals
α : Type ?u.806432
β : Type ?u.806435
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_le_coe, Real.toNNReal_le_toNNReal_iff h]