proposition: Lemma nth_parttuple_minn i sh1 sh2 : i < d.+1 -> nth 0 (parttuple_minn sh1 sh2) i = minn (sumn (take i sh1)) (sumn (take i sh2)).
proof: Proof. move=> ltid1. by rewrite -/(nat_of_ord (Ordinal ltid1)) nth_mktuple !tnth_mktuple /=. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype