proposition: Lemma pblockK x0 : {in X, cancel (pblock P) (transversal_repr x0 X)}.
proof: Proof. move=> x Xx; have /bigcupP[B PB Bx] := sXP Xx; rewrite (def_pblock tiP PB Bx). by apply/esym/set1P; rewrite -setI_transversal_pblock // inE Xx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)