proposition: Lemma setpart_shape_union P Q : [disjoint P & Q] -> setpart_shape (P :|: Q) = sort geq (setpart_shape P ++ setpart_shape Q).
proof: Proof. Proof using. rewrite /setpart_shape -setI_eq0 => /eqP disj. apply/perm_sortP/permP => // Prd. have count_sort l : count ^~ (sort geq l) =1 count ^~ l. by apply/permP; rewrite perm_sort perm_refl. rewrite count_cat !count_sort !count_set_of_card. rewrite setIUl cardsU -[RHS]subn0; congr(_ - _). apply/eqP; rewrite cards_eq0 -subset0 -disj. by apply/subsetP => x; rewrite !inE => /andP[/andP[-> _] /andP[-> _]]. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype