intro x y h
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
⊢ MulLECancellable (a * b)
α : Type u_1
inst✝¹ : LE α
inst✝ : Semigroup α
a b : α
ha : MulLECancellable a
hb : MulLECancellable b
x y : α
h : a * b * x ≤ a * b * y
⊢ x ≤ y