proposition: Lemma transversal_reprK x0 : {in P, cancel (transversal_repr x0 X) (pblock P)}.
proof: Proof. by move=> B PB; rewrite /= (def_pblock tiP PB) ?repr_mem_pblock. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)