proposition: Lemma card_inv_im (aT rT: finType) (f: aT -> rT) (A: {set aT}) (n: nat): (forall x, x \in A -> #|[set y in A | f x == f y]| = n) -> #|A| = #|f @: A| * n.
proof: Proof. pose g x := [set y in A | x == f y ]. have: {in f @: A &, injective g}. move => x y /imsetP [x' x'A ->] /imsetP [y' y'A ->] => eq. have: (x' \in (g (f x'))) by rewrite /g inE x'A eqxx. by rewrite eq inE => /andP [_] /eqP. move /imset_injP; rewrite -imset_comp; move /eqP => <- h. apply:card_uniform_partition. by move => a /imsetP [x xA ->]; rewrite - (h _ xA). exact: preim_partitionP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)