proposition: Lemma coefn_sum (I : Type) (r : seq I) (P : pred I) (F : I -> {poly_n R}) (k : nat) : (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
proof: Proof. by rewrite !raddf_sum //= coef_sum. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)