proposition: Lemma poly_of_qpoly_sum I (r : seq I) (P1 : pred I) (F : I -> {poly %/ h}) : ((\sum_(i <- r | P1 i) F i) = \sum_(p <- r | P1 p) ((F p) : {poly A}) :> {poly A})%R.
proof: Proof. by elim/big_rec2: _ => // i p q IH <-. 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)