[GOAL]
α : Type u_1
inst✝³ : Group α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
inst✝ : DenselyOrdered α
a b c : α
h : ∀ (ε : α), 1 < ε → a / ε ≤ b
ε : α
ε1 : ε < 1
⊢ a * ε ≤ b
[PROOFSTEP]
simpa only [div_eq_mul_inv, inv_inv] using h ε⁻¹ (Left.one_lt_inv_iff.2 ε1)
