proposition: Lemma card_injm A : A \subset D -> #|f @* A| = #|A|.
proof: Proof. move=> sAD; rewrite morphimEsub // card_in_imset //. exact: (sub_in2 (subsetP sAD) (injmP injf)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)