no goals
α : Type u_1
β : Type ?u.86235
inst✝² : LE α
inst✝¹ : CommSemigroup α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c : α
ha : MulLECancellable a
⊢ b * a ≤ c * a ↔ b ≤ c
rw [mul_comm b, mul_comm c, ha.mul_le_mul_iff_left]