proposition: Lemma ex_set_setpart_shape A (sh : 'P_#|A|) : exists2 P, partition P A & setpart_shape P = sh.
proof: Proof. Proof using. case: sh => sh. rewrite /is_part_of_n /= is_part_sortedE => /andP[/eqP shsum /andP[shsort]]. move=> /(ex_setpart_shape shsum) [P [Puniq Ppart Psh]]. exists [set X in P]; first exact: Ppart. apply (sorted_eq (leT := geq)) => //. - exact: sort_sorted. - rewrite /setpart_shape -Psh perm_sort; apply: perm_map. apply: (uniq_perm (enum_uniq [set X in P]) Puniq) => x. by rewrite mem_enum inE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype