no goals
α : Type u
inst✝³ : Group α
inst✝² : LT α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
inst✝ : CovariantClass α α (swap fun x x_1 => x * x_1) fun x x_1 => x < x_1
a✝ b c a : α
⊢ a / b < a / c ↔ c < b
rw [div_eq_mul_inv, div_eq_mul_inv, ← mul_lt_mul_iff_left a⁻¹, inv_mul_cancel_left,
  inv_mul_cancel_left, inv_lt_inv_iff]