proposition: Lemma imset_transversal_preim : f @: (transversal (preim_partition f D) D) = f @: D.
proof: Proof. have /and3P[/eqP Hcover Htriv _] := preim_partitionP f D. have Htr := transversalP (preim_partitionP f D). have /subsetP := transversal_sub Htr. move: Htr; set tr := transversal _ _ => Htr Hsub. apply/setP => y. apply/imsetP/imsetP => [] [x Hx ->{y}]; first by exists x; first apply Hsub. have := Hx; rewrite -{1}Hcover => HxD. exists (transversal_repr x tr (pblock (preim_partition f D) x)). - by apply: (repr_mem_transversal Htr); apply: pblock_mem. - apply/esym/eqP. move: HxD => /pblock_mem/(transversal_reprK Htr x)/eqP. rewrite eq_pblock //; first last. rewrite Hcover; apply/Hsub/(repr_mem_transversal Htr). by apply pblock_mem; rewrite Hcover. rewrite pblock_equivalence_partition //. + by split => // /eqP ->. + apply/Hsub/(repr_mem_transversal Htr). by apply pblock_mem; rewrite Hcover. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree