no goals
α : Type u_1
a b c d x y z : α
inst✝ : LinearOrderedCommGroupWithZero α
ha : a ≠ 0
hb : b ≠ 0
hc : c ≠ 0
⊢ a / b ≤ a / c ↔ c ≤ b
simp only [div_eq_mul_inv, mul_le_mul_left₀ ha, inv_le_inv₀ hb hc]