simp [npowRec, pow_succ]
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } = npowRec (Nat.succ n) { toFinsupp := a }
case succ
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
n_ih : { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ (Nat.succ n) a } =
    { toFinsupp := a } * npowRec n { toFinsupp := a }