proposition: Lemma eq_cpairZ : {in 'Z(H), cpairg1 =1 cpair1g \o gz}.
proof: Proof. rewrite /cpairg1 /cpair1g => z1 Zz1; set z2 := gz z1. have Zz2: z2 \in 'Z(K) by rewrite (subsetP sgzZZ) ?mem_morphim. have [[Gz1 _] [/= Gz2 _]]:= (setIP Zz1, setIP Zz2). do 2![case: restrmP => f /= [df _ _ _]; rewrite {f}df]. apply/rcoset_kerP; rewrite ?inE ?group1 ?andbT //. by rewrite ker_in_cprod mem_rcoset inE /= invg1 mulg1 mul1g Zz1 /=. 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)