no goals
α : Type ?u.304510
β : Type ?u.304513
a✝ b✝ c d : ℝ≥0∞
r✝ p q : ℝ≥0
a b : ℝ≥0∞
r : ℝ≥0
hr₀ : r ≠ 0
⊢ r⁻¹ • a ≤ b ↔ a ≤ r • b
simpa only [inv_inv] using (ENNReal.le_inv_smul_iff (inv_ne_zero hr₀)).symm