no goals
ι : Type ?u.144887
α : Type u_1
β : Type ?u.144893
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c < 0
⊢ a ≤ b / c ↔ b ≤ a * c
rw [← neg_neg c, mul_neg, div_neg, le_neg, div_le_iff (neg_pos.2 hc), neg_mul]