no goals
α : Type u
inst✝² : Group α
inst✝¹ : LinearOrder α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
h : ∀ (ε : α), 1 < ε → a < b * ε
h₁ : b < a
⊢ a < a
simpa using h _ (lt_inv_mul_iff_lt.mpr h₁)