proposition: Lemma xcprod_subproof : {gz : {morphism 'Z(H) >-> gt_ isob} | isom 'Z(H) 'Z(G_ isob) gz}.
proof: Proof. case: (pickP [pred f : {ffun _} | misom 'Z(H) 'Z(K) f]) => [f isoZ | no_f]. rewrite (misom_isog isoZ); case/andP: isoZ => fM isoZ. by exists [morphism of morphm fM]. move/pred0P: no_f => not_isoZ; rewrite [isob](congr1 negb not_isoZ). by exists (idm_morphism _); apply/isomP; rewrite injm_idm im_idm. 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)