proposition: Lemma polyOverP {p} : reflect (forall i, p`_i \in S) (p \in polyOver S).
proof: Proof. apply: (iffP (all_nthP 0)) => [Sp i | Sp i _]; last exact: Sp. by have [/Sp // | /(nth_default 0)->] := ltnP i (size p); apply: rpred0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)