proposition: Lemma take_intpartn_over sh i : d <= i -> take i sh = sh.
proof: Proof. move=> Hd; rewrite take_oversize // (leq_trans _ Hd) //. by rewrite -{2}(sumn_intpartn sh) size_part. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype