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