no goals
ι : Type ?u.150874
α : Type u_1
β : Type ?u.150880
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
ha : a < 0
hb : b < 0
⊢ a ≤ b⁻¹ ↔ b ≤ a⁻¹
rw [← inv_le_inv_of_neg (inv_lt_zero.2 hb) ha, inv_inv]