no goals
α : Type u
inst✝² : Group α
inst✝¹ : LE α
inst✝ : CovariantClass α α (fun x x_1 => x * x_1) fun x x_1 => x ≤ x_1
a b c d : α
⊢ 1 ≤ b⁻¹ * a ↔ b ≤ a
rw [← mul_le_mul_iff_left b, mul_one, mul_inv_cancel_left]