proposition: Lemma mem_pblock P x : (x \in pblock P x) = (x \in cover P).
proof: Proof. rewrite /pblock; apply/esym/bigcupP. case: pickP => /= [A /andP[PA Ax]| noA]; first by rewrite Ax; exists A. by rewrite inE => [[A PA Ax]]; case/andP: (noA A). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)