ι : Type ?u.30788
α : Type u_1
β : Type ?u.30794
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a / b ≤ c ↔ a ≤ b * c
ι : Type ?u.30788
α : Type u_1
β : Type ?u.30794
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ b⁻¹ * a ≤ c ↔ a ≤ b * c
rw [inv_eq_one_div, mul_comm, ← div_eq_mul_one_div]
no goals
ι : Type ?u.30788
α : Type u_1
β : Type ?u.30794
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
h : 0 < b
⊢ a / b ≤ c ↔ a ≤ b * c
exact div_le_iff' h