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⁻¹ < b / c ↔ c < a * b
rw [div_eq_mul_inv, lt_mul_inv_iff_mul_lt, inv_mul_lt_iff_lt_mul]