no goals
ι : Type ?u.181515
α : Type u_1
β : Type ?u.181521
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
h1 : a < 0
h2 : -1 < a
this : 1 / a < 1 / -1
⊢ 1 / a < -1
rwa [one_div_neg_one_eq_neg_one] at this