proposition: Lemma coef_nderivn n p i : p^`N(n)`_i = p`_(n + i) *+ 'C(n + i, n).
proof: Proof. rewrite coef_poly ltn_subRL; case: leqP => // le_p_ni. by rewrite nth_default ?mul0rn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)