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