proposition: Lemma polyOver_nderivn (ringS : semiringClosed R) : {in polyOver ringS, forall p n, p^`N(n) \in polyOver ringS}.
proof: Proof. move=> p /polyOverP Sp /= n; apply/polyOverP=> i. by rewrite coef_nderivn rpredMn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)