no goals
ι : Type ?u.177416
α : Type u_1
β : Type ?u.177422
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hb : b < 0
h : a ≤ b
⊢ 1 / b ≤ 1 / a
rwa [div_le_iff_of_neg' hb, ← div_eq_mul_one_div, div_le_one_of_neg (h.trans_lt hb)]