proposition: Lemma leq_morphim A : #|f @* A| <= #|A|.
proof: Proof. by apply: (leq_trans (leq_imset_card _ _)); rewrite subset_leq_card ?subsetIr. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)