proposition: Lemma horner_sum I (r : seq I) (P : pred I) F x : (\sum_(i <- r | P i) F i).[x] = \sum_(i <- r | P i) (F i).[x].
proof: Proof. by elim/big_rec2: _ => [|i _ p _ <-]; rewrite (horner0, hornerD). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)