rw [mul_assoc, mul_assoc] at h
α : 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
α : 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