proposition: Lemma nil_comm_properl G H A : nilpotent G -> H \subset G -> H :!=: 1 -> A \subset 'N_G(H) -> [~: H, A] \proper H.
proof: Proof. move=> nilG sHG ntH; rewrite subsetI properE; case/andP=> sAG nHA. rewrite (subset_trans (commgS H (subset_gen A))) ?commg_subl ?gen_subG //. apply: contra ntH => sHR; have:= forallP nilG H; rewrite subsetI sHG. by rewrite (subset_trans sHR) ?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)