proposition: Lemma morphim_injG : {in [pred G : {group aT} | 'ker f \subset G & G \subset D] &, injective (fun G => f @* G)}.
proof: Proof. move=> G H /andP[sKG sGD] /andP[sKH sHD] eqfGH. by apply: val_inj; rewrite /= -(morphimGK sKG sGD) eqfGH morphimGK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)