proposition: Lemma polyOverS (S1 S2 : {pred R}) : {subset S1 <= S2} -> {subset polyOver S1 <= polyOver S2}.
proof: Proof. by move=> sS12 p /(all_nthP 0)S1p; apply/(all_nthP 0)=> i /S1p; apply: sS12. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)