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