proposition: Lemma nilpotent_sub_norm G H : nilpotent G -> H \subset G -> 'N_G(H) \subset H -> G :=: H.
proof: Proof. move=> nilG sHG sNH; apply/eqP; rewrite eqEsubset sHG andbT; apply/negP=> nsGH. have{nsGH} [i sZH []]: exists2 i, 'Z_i(G) \subset H & ~ 'Z_i.+1(G) \subset H. case/ucnP: nilG => n ZnG; rewrite -{}ZnG in nsGH. elim: n => [|i IHi] in nsGH *; first by rewrite sub1G in nsGH. by case sZH: ('Z_i(G) \subset H); [exists i | apply: IHi; rewrite sZH]. apply: subset_trans sNH; rewrite subsetI ucn_sub -commg_subr. by apply: subset_trans sZH; apply: subset_trans (ucn_comm i G); apply: commgS. 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)