proposition: Lemma coef_sum I (r : seq I) (P : pred I) (F : I -> {poly R}) k : (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
proof: Proof. exact: (raddf_sum (coefp k)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)