proposition: Lemma norm_conj_cent A G x : x \in 'C(A) -> (A \subset 'N(G :^ x)) = (A \subset 'N(G)).
proof: Proof. by move=> cAx; rewrite norm_conj_norm ?(subsetP (cent_sub A)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)