proposition: Lemma ker_cprod_by_central : kerHK \subset 'Z(setX H K).
proof: Proof. rewrite -(center_dprod (setX_dprod H K)) -morphim_pairg1 -morphim_pair1g. rewrite -!injm_center ?subsetT ?injm_pair1g ?injm_pairg1 //=. rewrite morphim_pairg1 morphim_pair1g setX_dprod. apply/subsetP=> [[x y]] /[1!inE] /andP[Zx /eqP->]. by rewrite inE /= Zx groupV (subsetP sgzZZ) ?mem_morphim. 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)