proposition: Proposition coprime_quotient_cent A G H : H \subset G -> A \subset 'N(H) -> coprime #|G| #|A| -> solvable G -> 'C_G(A) / H = 'C_(G / H)(A / H).
proof: Proof. move=> sHG nHA coGA solG. have sRG: H :&: [~: G, A] \subset G by rewrite subIset ?sHG. by rewrite strongest_coprime_quotient_cent ?(coprimeSg sRG) 1?(solvableS sRG). 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)