ι : Type ?u.39811
α : Type u_1
β : Type ?u.39817
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ 1 / a ≤ b ↔ 1 ≤ a * b
ι : Type ?u.39811
α : Type u_1
β : Type ?u.39817
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ a * b
rw [inv_eq_one_div]
no goals
ι : Type ?u.39811
α : Type u_1
β : Type ?u.39817
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
⊢ 1 / a ≤ b ↔ 1 ≤ a * b
exact div_le_iff' ha