proposition: Lemma invariant_subnormal A G H : A \subset 'N(G) -> A \subset 'N(H) -> H <|<| G -> exists2 s, (A.-invariant).-series H s & last H s = G.
proof: Proof. move=> nGA nHA /andP[]; move: #|G| => m. elim: m => [|m IHm] in G nGA * => sHG. by rewrite eq_sym; exists [::]; last apply/eqP. rewrite iterSr; set K := <<_>>. have nKA: A \subset 'N(K) by rewrite norms_gen ?norms_class_support. have sHK: H \subset K by rewrite sub_gen ?sub_class_support. case/IHm=> // s Hsn defK; exists (rcons s G); last by rewrite last_rcons. rewrite rcons_path Hsn !andbA defK nGA nKA /= -/K. by rewrite gen_subG class_support_subG ?norms_gen ?class_support_norm. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)