proposition: Lemma polyOver_poly S n E : (forall i, i < n -> E i \in S) -> \poly_(i < n) E i \is a polyOver S.
proof: Proof. move=> S_E; apply/(all_nthP 0)=> i lt_i_p /=; rewrite coef_poly. by case: ifP => [/S_E// | /idP[]]; apply: leq_trans lt_i_p (size_poly n E). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)