proposition: Lemma pblock_notin P x : (pblock P x != set0) = (x \in S).
proof: Proof. apply/idP/idP => [/set0Pn[y]|]. by rewrite mem_pblockC // => /mem_pblock_setpart. rewrite -{1}(cover_setpart P) => /pblock_mem H. by have:= setpart_non0 P; apply contra=> /eqP <-. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition