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 : α
⊢ a⁻¹ < 1 ↔ 1 < a
rw [← mul_lt_mul_iff_right a, inv_mul_self, one_mul]