proposition: Lemma nil_comm_properr G A H : nilpotent G -> H \subset G -> H :!=: 1 -> A \subset 'N_G(H) -> [~: A, H] \proper H.
proof: Proof. by rewrite commGC; apply: nil_comm_properl. 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)