proposition: Lemma morphimGK G : 'ker f \subset G -> G \subset D -> f @*^-1 (f @* G) = G.
proof: Proof. by move=> sKG sGD; rewrite morphimK // mulSGid. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)