no goals
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b c d : α
⊢ a * b⁻¹ < c ↔ a < b * c
rw [← inv_mul_lt_iff_lt_mul, mul_comm]