intro x y h
α : 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)
⊢ MulLECancellable b
α : 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
⊢ x ≤ y