proposition: Lemma card_preim_partition : #|preim_partition f D| = #|f @: D|.
proof: Proof. have Htr := transversalP (preim_partitionP f D). have /subsetP := transversal_sub Htr. rewrite -(card_transversal Htr) -imset_transversal_preim. move: (transversal _ _ ) Htr => tr Htr Hsub. apply/esym/card_in_imset => x y Hx Hy Heq. apply: (pblock_inj Htr Hx Hy); apply same_pblock. by have /and3P[] := preim_partitionP f D. rewrite pblock_equivalence_partition ?Heq //; try exact: Hsub. by split => // /eqP ->. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(div ssralg ssrint ssrnum binomial) tools combclass bintree