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