proposition: Lemma coef_add_seqpoly (sp sq : seqpoly R) (i : nat) : (sp + sq)%C`_i = sp`_i + sq`_i.
proof: Proof. elim: sp sq i=> [sq i|a p ihp [|b q] [|i]] //=. by rewrite [(_ + _)%C]/add_seqpoly /add_seqpoly_fun nth_nil add0r. by rewrite addr0. by rewrite addr0. by rewrite ihp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)