α : Type ?u.292307
β : Type ?u.292310
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : b ≤ a * c
⊢ b / c ≤ a
α : Type ?u.292307
β : Type ?u.292310
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a < b / c
⊢ a * c < b
contrapose! h
no goals
α : Type ?u.292307
β : Type ?u.292310
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : b ≤ a * c
⊢ b / c ≤ a
exact ENNReal.div_le_of_le_mul h