proposition: Lemma coprime_norm_cent A G : A \subset 'N(G) -> coprime #|G| #|A| -> 'N_G(A) = 'C_G(A).
proof: Proof. move=> nGA coGA; apply/eqP; rewrite eqEsubset andbC setIS ?cent_sub //=. rewrite subsetI subsetIl /= (sameP commG1P trivgP) -(coprime_TIg coGA). rewrite subsetI commg_subr subsetIr andbT. move: nGA; rewrite -commg_subl; apply: subset_trans. by rewrite commSg ?subsetIl. 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)