proposition: Lemma polyOver_comp (ringS : semiringClosed R) : {in polyOver ringS &, forall p q, p \Po q \in polyOver ringS}.
proof: Proof. move=> p q /polyOverP Sp Sq; rewrite comp_polyE rpred_sum // => i _. by rewrite polyOverZ ?rpredX. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)