proposition: Lemma sum_poly_weaken (l : {poly K}) s : (size l <= s)%nat -> \sum_(0 <= i < s) l`_i = \sum_(i < size l) l`_i.
proof: Proof. move=> Hl. rewrite -{1}(subnKC Hl) // {1}/index_iota subn0 iotaD big_cat /=. rewrite -{1}(subn0 (size l)) big_mkord // -[RHS]addr0; congr (_ + _). rewrite big_nat_cond big1 // add0n => i /andP[/andP[Hi _] _]. by apply/leq_sizeP : Hi. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist