proposition: Lemma subnormalP H G : reflect (exists2 s, normal.-series H s & last H s = G) (H <|<| G).
proof: Proof. apply: (iffP andP) => [[sHG snHG] | [s Hsn <-{G}]]. move: #|G| snHG => m; elim: m => [|m IHm] in G sHG *. by exists [::]; last by apply/eqP; rewrite eq_sym. rewrite iterSr => /IHm[|s Hsn defG]. by rewrite sub_gen // class_supportEr (bigD1 1) //= conjsg1 subsetUl. exists (rcons s G); rewrite ?last_rcons // -cats1 cat_path Hsn defG /=. rewrite /normal gen_subG class_support_subG //=. by rewrite norms_gen ?class_support_norm. set f := fun _ => <<_>>; have idf: iter _ f H == H. by elim=> //= m IHm; rewrite (eqP IHm) /f class_support_id genGid. have [m] := ubnP (size s); elim: m s Hsn => // m IHm /lastP[//|s G]. rewrite size_rcons last_rcons rcons_path /= ltnS. set K := last H s => /andP[Hsn /andP[sKG nKG]] lt_s_m. have /[1!subEproper]/predU1P[<-|prKG] := sKG; first exact: IHm. pose L := [group of f G]. have sHK: H \subset K by case/IHm: Hsn. have sLK: L \subset K by rewrite gen_subG class_support_sub_norm. rewrite -(subnK (proper_card (sub_proper_trans sLK prKG))) iterD iterSr. have defH: H = setIgr L H by rewrite -sub_setIgr ?sub_gen ?sub_class_support. have: normal.-series H (map (setIgr L) s) by rewrite defH path_setIgr. case/IHm=> [|_]; first by rewrite size_map. rewrite [in last _]defH last_map (subset_trans sHK) //=. by rewrite (setIidPr sLK) => /eqP->. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action commutator center)