proposition: Lemma coef_deriv p i : p^`()`_i = p`_i.+1 *+ i.+1.
proof: Proof. rewrite coef_poly -subn1 ltn_subRL. by case: leqP => // /(nth_default 0) ->; rewrite mul0rn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)