proposition: Lemma center_prod H K : K \subset 'C(H) -> 'Z(H) * 'Z(K) = 'Z(H * K).
proof: Proof. move=> cHK; apply/setP=> z; rewrite {3}/center centM !inE. have cKH: H \subset 'C(K) by rewrite centsC. apply/imset2P/and3P=> [[x y /setIP[Hx cHx] /setIP[Ky cKy] ->{z}]| []]. by rewrite imset2_f ?groupM // ?(subsetP cHK) ?(subsetP cKH). case/imset2P=> x y Hx Ky ->{z}. rewrite groupMr => [cHx|]; last exact: subsetP Ky. rewrite groupMl => [cKy|]; last exact: subsetP Hx. by exists x y; rewrite ?inE ?Hx ?Ky. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(cyclic)