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