proposition: Lemma center_dprod A B G : A \x B = G -> 'Z(A) \x 'Z(B) = 'Z(G).
proof: Proof. case/dprodP=> [[H1 H2 -> ->] defG cH12 trH12]. move: defG; rewrite -cprodE // => /center_cprod/cprodP[_ /= <- cZ12]. by apply: dprodE; rewrite //= setIAC setIA -setIA trH12 (setIidPl _) ?sub1G. 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)