proposition: Lemma nilpotent_proper_norm G H : nilpotent G -> H \proper G -> H \proper 'N_G(H).
proof: Proof. move=> nilG; rewrite properEneq properE subsetI normG => /andP[neHG sHG]. by rewrite sHG; apply: contra neHG => /(nilpotent_sub_norm nilG)->. 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)