no goals
ι : Type ?u.193207
α : Type u_1
β : Type ?u.193213
inst✝ : LinearOrderedField α
a b c d : α
n : ℤ
hc : c ≠ 0
hd : d ≠ 0
⊢ (a * d - b * c) / (c * d) ≤ 0 ↔ a / c ≤ b / d
rw [mul_comm b c, ← div_sub_div _ _ hc hd, sub_nonpos]