proposition: Proposition coprimeR_cent_prod gT (A G : {group gT}) : A \subset 'N(G) -> coprime #|[~: G, A]| #|A| -> solvable [~: G, A] -> [~: G, A] * 'C_G(A) = G.
proof: Proof. move=> nGA coRA solR; apply/eqP; rewrite eqEsubset mulG_subG commg_subl nGA. rewrite subsetIl -quotientSK ?commg_norml //=. rewrite coprime_norm_quotient_cent ?commg_normr //=. by rewrite subsetI subxx quotient_cents2r. 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)