proposition: Lemma pblock_setpart1 x : x \in S -> pblock setpart1 x = [set x].
proof: Proof. move=> xinS; apply: (def_pblock (trivIsetpart _)); rewrite ?inE //. by rewrite /setpart1 /= imset_f. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition