proposition: Lemma transversalP P D : partition P D -> is_transversal (transversal P D) P D.
proof: Proof. case/and3P=> /eqP <- tiP notP0; apply/and3P; split; first exact/and3P. apply/subsetP=> _ /imsetP[x Px ->]; case: pickP => //= y Pxy. by apply/bigcupP; exists (pblock P x); rewrite ?pblock_mem //. apply/forall_inP=> B PB; have /set0Pn[x Bx]: B != set0 := memPn notP0 B PB. apply/cards1P; exists (odflt x [pick y in pblock P x]); apply/esym/eqP. rewrite eqEsubset sub1set !inE -andbA; apply/andP; split. by apply/imset_f/bigcupP; exists B. rewrite (def_pblock tiP PB Bx); case def_y: _ / pickP => [y By | /(_ x)/idP//]. rewrite By /=; apply/subsetP=> _ /setIP[/imsetP[z Pz ->]]. case: {1}_ / pickP => [t zPt Bt | /(_ z)/idP[]]; last by rewrite mem_pblock. by rewrite -(same_pblock tiP zPt) (def_pblock tiP PB Bt) def_y inE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(choice fintype finfun bigop)