proposition: Lemma from_parttupleP t : is_parttuple t -> is_part_of_n d (from_parttuple t).
proof: Proof. move=> /is_parttupleP[t0 td srt conv]. have {}t0 : nth 0 t 0 = 0 by move: t0; rewrite (tnth_nth 0). have {}td : nth 0 t d = d by move: td; rewrite (tnth_nth 0). apply/andP; split. rewrite sumn_rem_trail0 sumnE big_map. by rewrite -{1}(subn0 d) -/(index_iota _ _) sum_diff_tuple // t0 td subn0. move: srt => /(sortedP 0) srt. apply: is_part_rem_trail0; apply/(sortedP 0) => i /=. rewrite size_map size_iota => H1. have Hi1 : i.+1 < d.+1 by apply ltnW. rewrite !(nth_map 0) ?size_iota ?nth_iota // add0n. rewrite leq_subLR addnBA ?srt ?size_tuple // add0n addnn. rewrite leq_subRL ?conv // -addnn. apply: (leq_trans (srt _ _) (leq_addr _ _)). by rewrite size_tuple. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype