proposition: Lemma horner_Poly s x : (Poly s).[x] = horner_rec s x.
proof: Proof. by elim: s => [|a s /= <-]; rewrite (horner0, horner_cons). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)