proposition: Lemma subcent_dprod B C G A : B \x C = G -> A \subset 'N(B) :&: 'N(C) -> 'C_B(A) \x 'C_C(A) = 'C_G(A).
proof: Proof. move=> defG; have [_ _ cBC _] := dprodP defG; move: defG. by rewrite !dprodEsd 1?(centSS _ _ cBC) ?subsetIl //; apply: subcent_sdprod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)