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