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