rw [mul_assoc, mul_assoc]
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * b * x ≤ a * b * y
case a
α : Type u_1
inst✝² : LE α
inst✝¹ : Semigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b : α
hab : MulLECancellable (a * b)
x y : α
h : b * x ≤ b * y
⊢ a * (b * x) ≤ a * (b * y)