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