no goals
ι : Type ?u.65810
α : Type u_1
β : Type ?u.65816
inst✝ : LinearOrderedSemifield α
a b c d e : α
m n : ℤ
ha : 0 < a
hb : 0 < b
hc : 0 < c
⊢ a / b < a / c ↔ c < b
simp only [div_eq_mul_inv, mul_lt_mul_left ha, inv_lt_inv hb hc]