proposition: Lemma setpart_shapeP P D : partition P D -> is_part_of_n #|D| (setpart_shape P).
proof: Proof. Proof using. rewrite /setpart_shape => /and3P[/eqP Hcov Htriv Hnon0]. rewrite /is_part_of_n /= is_part_sortedE. apply/and3P; split. - by rewrite sumn_sort sumnE big_map big_enum -Hcov. - exact: sort_sorted. - move: Hnon0; apply contra. rewrite mem_sort => /mapP[x]. by rewrite mem_enum => Hx /esym/cards0_eq <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype