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