proposition: Lemma morphim_subnormal (rT : finGroupType) G (f : {morphism G >-> rT}) H K : H <|<| K -> f @* H <|<| f @* K.
proof: Proof. case/subnormalP => s Hs <-{K}; apply/subnormalP. elim: s H Hs => [|K s IHs] H /=; first by exists [::]. case/andP=> nsHK /IHs[fs Hfs <-]. by exists ([group of f @* K] :: fs); rewrite /= ?morphim_normal. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)