proposition: Lemma sumn_take_part_fromtuple t (H : is_parttuple t) i : i < d.+1 -> sumn (take i (part_fromtuple H)) = nth 0 t i.
proof: Proof. rewrite /part_fromtuple /from_parttuple /= => Hi. move/is_parttupleP : H => [t0 _ srt _]. have {}t0 : nth 0 t 0 = 0 by move: t0; rewrite (tnth_nth 0). rewrite sumn_take big_nat. under eq_bigr => j /= Hj. have lejd : j < d by rewrite (leq_trans Hj) // -ltnS. by rewrite nth_rem_trail0 (nth_map 0) ?size_iota // nth_iota // over. by rewrite -big_nat sum_diff_tuple // t0 subn0. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype