proposition: Lemma injm_maxnormal : maxnormal (f @* M) (f @* G) (f @* L) = maxnormal M G L.
proof: Proof. pose injfm := (injm_proper injf, injm_norms, injmSK injf, subsetIl). apply/maxgroupP/maxgroupP; rewrite !injfm // => [[nML maxM]]. split=> // H nHL sMH; have [/proper_sub sHG _] := andP nHL. have dH := subset_trans sHG dG; apply: (injm_morphim_inj injf) => //. by apply: maxM; rewrite !injfm. split=> // fH nHL sMH; have [/proper_sub sfHG _] := andP nHL. have{sfHG} dfH: fH \subset f @* D := subset_trans sfHG (morphim_sub f G). by rewrite -(morphpreK dfH) !injfm // in nHL sMH *; rewrite (maxM _ nHL). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)