proposition: Lemma morphim_injm_eq1 A : A \subset D -> (f @* A == 1) = (A == 1).
proof: Proof. by move=> sAD; rewrite -morphim1 injm_eq ?sub1G. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)