proposition: Lemma quotient_TI_subcent K G H : G \subset 'N(K) -> G \subset 'N(H) -> K :&: H = 1 -> 'C_K(G) / H = 'C_(K / H)(G / H).
proof: Proof. move=> nGK nGH tiKH. have tiHR: H :&: [~: K, G] = 1. by apply/trivgP; rewrite /= setIC -tiKH setSI ?commg_subl. apply: strongest_coprime_quotient_cent; rewrite ?tiHR ?sub1G ?solvable1 //. by rewrite cards1 coprime1n. 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)