proposition: Lemma subnormalEl G H : H <|<| G -> H :=: G \/ (exists K : {group gT}, [/\ H <| K, K <|<| G & H \proper K]).
proof: Proof. case/subnormalP=> s Hs <-{G}; elim: s H Hs => /= [|K s IHs] H; first by left. case/andP=> nsHK Ks; have /[1!subEproper] := normal_sub nsHK. case/predU1P=> [-> | prHK]; [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)