proposition: Lemma ex_setpart_shape (s : seq nat) (A : {set T}) : sumn s = #|A| -> 0 \notin s -> exists P : seq {set T}, [/\ uniq P, partition [set X in P] A & [seq #{X} | X <- P] = s].
proof: Proof. Proof using. elim: s A => [| i s IHs] A /=. move=> /esym/cards0_eq -> _; exists [::]; split => //. by rewrite partition_set0. rewrite inE eq_sym => Hi /norP[Bne0 {}/IHs Hrec]. have: i <= #|A| by rewrite -Hi; apply: leq_addr. move=> /ex_subset_card [B BsubA /eqP cardB]; subst i. have {}/Hrec [P [Puniq]] : sumn s = #|A :\: B|. by rewrite cardsD (setIidPr BsubA) -Hi addKn. move=> /and3P[/eqP covP trivP set0P] Ps; rewrite inE in set0P. have BninP : B \notin P. move: Bne0; apply contra => BinP; rewrite cards_eq0. have : B \subset A :\: B. by rewrite -covP /cover; apply (bigcup_max B); rewrite // inE. rewrite setDE => /subsetIP[_]. by rewrite -disjoints_subset -setI_eq0 setIid. rewrite -lt0n card_gt0 in Bne0. have Hcons : [set X in B :: P] = B |: [set X in P]. by apply/setP => X; rewrite !inE. exists (B :: P); split => /=; [|apply/and3P; split|]. - by rewrite Puniq BninP. - rewrite Hcons /cover big_setU1 /= ?inE // -/(cover _) covP. by rewrite -{1}(setIidPr BsubA) setID. - move: trivP; rewrite /trivIset Hcons. rewrite /cover !big_setU1 ?inE //= -/(cover _) => /eqP ->. rewrite covP cardsU (_ : B :&: (A :\: B) = set0) ?cards0 ?subn0 //. by rewrite setDE setIC -setIA [X in A :&: X]setIC setICr setI0. - by rewrite !inE negb_or eq_sym Bne0. - by rewrite Ps. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype