no goals
ι : Type ?u.68484
α : Type u_1
β : Type ?u.68490
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
b0 : 0 < b
d0 : 0 < d
⊢ a / b ≤ c / d ↔ a * d ≤ c * b
rw [le_div_iff d0, div_mul_eq_mul_div, div_le_iff b0]