proposition: Lemma coprime_norm_quotient_cent A G H : A \subset 'N(G) -> A \subset 'N(H) -> coprime #|H| #|A| -> solvable H -> 'C_G(A) / H = 'C_(G / H)(A / H).
proof: Proof. move=> nGA nHA coHA solH; have sRH := subsetIl H [~: G, A]. rewrite strongest_coprime_quotient_cent ?(coprimeSg sRH) 1?(solvableS sRH) //. by rewrite subIset // commg_subl nGA orbT. 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)