no goals
ι : Type ?u.83513
α : Type u_1
β : Type ?u.83519
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
h : a < b
⊢ 1 / b < 1 / a
rwa [lt_div_iff' ha, ← div_eq_mul_one_div, div_lt_one (ha.trans h)]