no goals
ι : Type ?u.178065
α : Type u_1
β : Type ?u.178071
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
h : a < b
⊢ 1 / b < 1 / a
rwa [div_lt_iff_of_neg' hb, ← div_eq_mul_one_div, div_lt_one_of_neg (h.trans hb)]