proposition: Lemma xcprodP : 'Z(H) \isog 'Z(K) -> xcprod_spec xcprod.
proof: Proof. by rewrite /xcprod => isoZ; move: xcprod_subproof; rewrite isoZ. 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)