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