no goals
M : Type ?u.8183
N : Type u_1
S : Type ?u.8189
M₀ : Type ?u.8192
M₁ : Type ?u.8195
R : Type ?u.8198
G : Type ?u.8201
G₀ : Type ?u.8204
inst✝⁷ : Mul M
inst✝⁶ : Monoid N
inst✝⁵ : Semigroup S
inst✝⁴ : MulZeroClass M₀
inst✝³ : MulOneClass M₁
inst✝² : NonAssocRing R
inst✝¹ : Group G
inst✝ : CancelMonoidWithZero G₀
p : N
n✝ : ℕ
h : IsIdempotentElem p
n : ℕ
ih : p ^ (n + 1) = p
⊢ p ^ (Nat.succ n + 1) = p
rw [pow_succ, ih, h.eq]