proposition: Fact nderivn_is_linear n : linear (nderivn n).
proof: Proof. move=> k p q; apply/polyP=> i. by rewrite !(coef_nderivn, coefD, coefZ) mulrnDl mulrnAr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)