proposition: Lemma mem_pblock_setpart P x y : x \in pblock P y -> x \in S.
proof: Proof. move=> /[dup] xPy. by rewrite -(same_pblock (trivIsetpart P) xPy) mem_pblock cover_setpart. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition