proposition: Lemma setI_im_cpair : CH :&: CK = 'Z(CH).
proof: Proof. apply/eqP; rewrite eqEsubset setIS //=. rewrite subsetI center_sub -injm_center //. rewrite (eq_in_morphim _ eq_cpairZ); first by rewrite morphim_comp morphimS. by rewrite !(setIidPr _) // -sub_morphim_pre. 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)