proposition: Lemma rpred_horner : {in polyOver S & S, forall p x, p.[x] \in S}.
proof: Proof. move=> p x /polyOverP Sp Sx; rewrite horner_coef rpred_sum // => i _. by rewrite rpredM ?rpredX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)