proposition: Lemma pblock_transversal : pblock P @: X = P.
proof: Proof. apply/setP=> B; apply/imsetP/idP=> [[x Xx ->] | PB]. by rewrite pblock_mem ?sXP. have /cards1P[x0 _] := trX PB; set x := transversal_repr x0 X B. by exists x; rewrite ?transversal_reprK ?repr_mem_transversal. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)