proposition: Lemma def_pblock P B x : trivIset P -> B \in P -> x \in B -> pblock P x = B.
proof: Proof. move/trivIsetP=> tiP PB Bx; have Px: x \in cover P by apply/bigcupP; exists B. apply: (contraNeq (tiP _ _ _ PB)); first by rewrite pblock_mem. by apply/pred0Pn; exists x; rewrite /= mem_pblock Px. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)