proposition: Lemma ucn_cprod n A B G : A \* B = G -> 'Z_n(A) \* 'Z_n(B) = 'Z_n(G).
proof: Proof. case/cprodP=> [[H K -> ->{A B}] mulHK cHK]. elim: n => [|n /cprodP[_ /= defZ cZn]]; first exact: cprod1g. set Z := 'Z_n(G) in defZ cZn; rewrite (ucnSn n G) /= -/Z. have /mulGsubP[nZH nZK]: H * K \subset 'N(Z) by rewrite mulHK gFnorm. have <-: 'Z(H / Z) * 'Z(K / Z) = 'Z(G / Z). by rewrite -mulHK quotientMl // center_prod ?quotient_cents. have ZquoZ (B A : {group gT}): B \subset 'C(A) -> 'Z_n(A) * 'Z_n(B) = Z -> 'Z(A / Z) = 'Z_n.+1(A) / Z. - move=> cAB {}defZ; have cAZnB: 'Z_n(B) \subset 'C(A) := gFsub_trans _ cAB. have /second_isom[/=]: A \subset 'N(Z). by rewrite -defZ normsM ?gFnorm ?cents_norm // centsC. suffices ->: Z :&: A = 'Z_n(A). by move=> f inj_f im_f; rewrite -!im_f ?gFsub // ucn_central injm_center. rewrite -defZ -group_modl ?gFsub //; apply/mulGidPl. have [-> | n_gt0] := posnP n; first exact: subsetIl. by apply: subset_trans (ucn_sub_geq A n_gt0); rewrite /= setIC ucn1 setIS. rewrite (ZquoZ H K) 1?centsC 1?(centC cZn) // {ZquoZ}(ZquoZ K H) //. have cZn1: 'Z_n.+1(K) \subset 'C('Z_n.+1(H)) by apply: centSS cHK; apply: gFsub. rewrite -quotientMl ?quotientK ?mul_subG ?gFsub_trans //=. rewrite cprodE // -cent_joinEr ?mulSGid //= cent_joinEr //= -/Z. by rewrite -defZ mulgSS ?ucn_subS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)