proposition: Lemma mem_morphim A x : x \in D -> x \in A -> f x \in f @* A.
proof: Proof. by move=> Dx Ax; apply/morphimP; exists x. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)