proposition: Lemma cpairg1_center : cpairg1 @* 'Z(H) = 'Z(C).
proof: Proof. by rewrite -cpair1g_center !injm_center // cpair_center_id. 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)