proposition: Lemma inj_card_preimset (aT rT : finType) (f : aT -> rT) (A : {set rT}) : injective f -> A \subset codom f -> #|f @^-1: A| = #|A|.
proof: Proof. move=> inj_f /subsetP => subAf. have [->|[y yA]] := set_0Vmem A; first by rewrite preimset0 !cards0. have x0 : aT := (iinv (subAf _ yA)). pose g (x : rT) : aT := if @idP (x \in codom f) is ReflectT p then iinv p else x0. apply: on_card_preimset; exists g. - by move => x /subAf; rewrite /g; case E : {1}_ / idP; rewrite // iinv_f. - by move => x /subAf; rewrite /g; case E : {1}_ / idP; rewrite // f_iinv. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone)