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