proposition: Lemma im_cpair : CH * CK = C.
proof: Proof. rewrite /cpairg1 /cpair1g; do 2!case: restrmP => _ [_ _ _ -> //]. rewrite !morphim_comp -morphimMl morphim_pairg1 ?setXS ?sub1G //. rewrite morphim_pair1g setX_prod morphimEdom /= /in_cprod /cprod_by. by case: cprod_by_key; rewrite /= imset_comp imset_coset -morphimEdom im_subg. 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)