proposition: Lemma card_im_injm : (#|f @* D| == #|D|) = 'injm f.
proof: Proof. by rewrite morphimEdom (sameP imset_injP injmP). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)