proposition: Proposition coprime_cent_Phi gT p (A G : {group gT}) : p.-group G -> coprime #|G| #|A| -> [~: G, A] \subset 'Phi(G) -> A \subset 'C(G).
proof: Proof. move=> pG coGA sRphi; rewrite centsC; apply/setIidPl. rewrite -['C_G(A)]genGid; apply/Phi_nongen/eqP. rewrite eqEsubset join_subG Phi_sub subsetIl -genM_join sub_gen //=. rewrite -{1}(coprime_cent_prod _ coGA) ?(pgroup_sol pG) ?mulSg //. by rewrite -commg_subl (subset_trans sRphi) ?Phi_sub. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)