no goals
α : Type u_1
inst✝ : AddCommMonoid α
c n : ℕ
x a : α
n' : ℕ
a' : α
h₁ : c * n = n'
h₂ : smul c a = a'
⊢ smul c (term n x a) = term n' x a'
simp [h₂.symm, h₁.symm, term, smul, nsmul_add, mul_nsmul']