proposition: Lemma size_nderivn (R : realDomainType) (p : {poly R}) n : size p^`N(n) = (size p - n)%N.
proof: Proof. rewrite -size_derivn nderivn_def -mulr_natl. by rewrite -polyC1 -!polyCMn size_Cmul // pnatr_eq0 -lt0n fact_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)