α : Type u_1
β : Type ?u.49483
ι : Type ?u.49486
π : ι → Type ?u.49491
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a * a ^ n ≤ a∗
α : Type u_1
β : Type ?u.49483
ι : Type ?u.49486
π : ι → Type ?u.49491
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a ^ (n + 1) ≤ a∗
rw [pow_succ]
no goals
α : Type u_1
β : Type ?u.49483
ι : Type ?u.49486
π : ι → Type ?u.49491
inst✝ : KleeneAlgebra α
a b c : α
n : ℕ
⊢ a * a ^ n ≤ a∗
exact (mul_le_mul_left' pow_le_kstar _).trans mul_kstar_le_kstar