no goals
α : Type u_1
β : Type ?u.23306
inst✝² : MulOneClass α
inst✝¹ : LT α
inst✝ : ContravariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x < x_1
a b : α
h : a * b < a
⊢ ?m.23646 h * b < ?m.23646 h * 1
simpa only [mul_one]