proposition: Lemma subcent_sdprod B C G A : B ><| C = G -> A \subset 'N(B) :&: 'N(C) -> 'C_B(A) ><| 'C_C(A) = 'C_G(A).
proof: Proof. case/sdprodP=> [[H K -> ->] <- nHK tiHK] nHKA {B C G}. rewrite sdprodE ?subcent_TImulg ?normsIG //. by rewrite -setIIl tiHK (setIidPl (sub1G _)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)