proposition: Lemma pblock_in (T : finType) (P : {set {set T}}) (x : T) : set0 \notin P -> (pblock P x \in P) = (x \in cover P).
proof: Proof. move=> set0nP; rewrite /pblock; apply/esym/bigcupP. case: pickP=> /= [A /andP[PA Ax]| noA]; first by rewrite PA; exists A. by rewrite (negbTE set0nP)=> [[A PA Ax]]; case/andP: (noA A). Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass sorted ordtype partition