proposition: Lemma im_cpair_cent : CK \subset 'C(CH).
proof: Proof. rewrite /cpairg1 /cpair1g; do 2!case: restrmP => _ [_ _ _ -> //]. rewrite !morphim_comp morphim_cents // morphim_pair1g morphim_pairg1. by case/dprodP: (setX_dprod H K). 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)