induction n with
| zero        => simp [npowRec]; rfl
| succ n n_ih => simp [npowRec, pow_succ]; rw [<- n_ih, <- ofFinsupp_mul]; rfl
R : Type u
a✝ b : R
m n✝ : ℕ
inst✝ : Semiring R
φ : R →+* R
p q : R[X;φ]
a : AddMonoidAlgebra R ℕ
n : ℕ
⊢ { toFinsupp := SkewPolynomial.AddMonoidAlgebra.pow' φ n a } = npowRec n { toFinsupp := a }
no goals