no goals
ι : Type ?u.149888
α : Type u_1
β : Type ?u.149894
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a⁻¹ ≤ b⁻¹ ↔ b ≤ a
rw [← one_div, div_le_iff_of_neg ha, ← div_eq_inv_mul, div_le_iff_of_neg hb, one_mul]