proposition: Lemma setI_transversal_pblock x0 B : B \in P -> X :&: B = [set transversal_repr x0 X B].
proof: Proof. by case/trX/cards1P=> x defXB; rewrite /transversal_repr defXB /pick enum_set1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)