proposition: Lemma subnormalEr G H : H <|<| G -> H :=: G \/ (exists K : {group gT}, [/\ H <|<| K, K <| G & K \proper G]).
proof: Proof. case/subnormalP=> s Hs <-{G}. elim/last_ind: s Hs => [|s G IHs]; first by left. rewrite last_rcons -cats1 cat_path /= andbT; set K := last H s. case/andP=> Hs nsKG; have /[1!subEproper] := normal_sub nsKG. case/predU1P=> [<- | prKG]; [exact: IHs | right; exists K; split=> //]. by apply/subnormalP; exists s. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)