proposition: Lemma injm_minnormal : minnormal (f @* M) (f @* G) = minnormal M G.
proof: Proof. pose injfm := (morphim_injm_eq1 injf, injm_norms, injmSK injf, subsetIl). apply/mingroupP/mingroupP; rewrite !injfm // => [[nML minM]]. split=> // H nHG sHM; have dH := subset_trans sHM dM. by apply: (injm_morphim_inj injf) => //; apply: minM; rewrite !injfm. split=> // fH nHG sHM; have dfH := subset_trans sHM (morphim_sub f M). by rewrite -(morphpreK dfH) !injfm // in nHG sHM *; rewrite (minM _ nHG). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)