proposition: Lemma mem_setpart_pblock P A : A \in P -> exists x, x \in A.
proof: Proof. move=> AinP. have /set0Pn[x xinA] : A != set0. by move: (setpart_non0 P); apply contra=> /eqP <-. by exists x. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition