α : Type ?u.290686
β : Type ?u.290689
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b / c
⊢ a * c⁻¹⁻¹ ≤ b
α : Type ?u.290686
β : Type ?u.290689
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b / c
⊢ a * c ≤ b
rw [← inv_inv c]
no goals
α : Type ?u.290686
β : Type ?u.290689
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b / c
⊢ a * c⁻¹⁻¹ ≤ b
exact div_le_of_le_mul h