no goals
ι : Type ?u.182424
α : Type u_1
β : Type ?u.182430
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