proposition: Lemma repr_mem_pblock x0 B : B \in P -> transversal_repr x0 X B \in B.
proof: Proof. by move=> PB; rewrite -sub1set -setI_transversal_pblock ?subsetIr. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)