proposition: Lemma derivn_poly0 p n : size p <= n -> p^`(n) = 0.
proof: Proof. move=> le_p_n; apply/polyP=> i; rewrite coef_derivn. rewrite nth_default; first by rewrite mul0rn coef0. exact/(leq_trans le_p_n)/leq_addr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)