proposition: Lemma nilpotent_subnormal G H : nilpotent G -> H \subset G -> H <|<| G.
proof: Proof. move=> nilG; have [m] := ubnP (#|G| - #|H|). elim: m H => // m IHm H /ltnSE-leGHm sHG. have [->|] := eqVproper sHG; first exact: subnormal_refl. move/(nilpotent_proper_norm nilG); set K := 'N_G(H) => prHK. have snHK: H <|<| K by rewrite normal_subnormal ?normalSG. have sKG: K \subset G by rewrite subsetIl. apply: subnormal_trans snHK (IHm _ (leq_trans _ leGHm) sKG). by rewrite ltn_sub2l ?proper_card ?(proper_sub_trans prHK). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)