proposition: Lemma sum_drop_poly n p : \sum_(n <= i < size p) p`_i *: 'X^i = drop_poly n p * 'X^n.
proof: Proof. rewrite (big_addn 0) big_mkord /drop_poly poly_def mulr_suml. by apply: eq_bigr => i _; rewrite exprD scalerAl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype bigop finset tuple) mathcomp(div ssralg countalg binomial)