proposition: Lemma pmorphim_pgroup pi G : pi.-group ('ker f) -> G \subset D -> pi.-group (f @* G) = pi.-group G.
proof: Proof. move=> piker sGD; apply/idP/idP=> [pifG|]; last exact: morphim_pgroup. apply: (@pgroupS _ _ (f @*^-1 (f @* G))); first by rewrite -sub_morphim_pre. by rewrite /pgroup card_morphpre ?morphimS // pnatM; apply/andP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)