proposition: Lemma nth_parttuple i sh : i < d.+1 -> nth 0 (parttuple sh) i = sumn (take i sh).
proof: Proof. by move=> ltid1; rewrite (nth_map ord0) ?size_enum_ord ?nth_enum_ord. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype