proposition: Lemma isog_xcprod (rT : finGroupType) (GH GK G : {group rT}) : Aut_in (Aut H) 'Z(H) \isog Aut 'Z(H) -> GH \isog H -> GK \isog K -> GH \* GK = G -> 'Z(GH) = 'Z(GK) -> G \isog [set: xcprod].
proof: Proof. move=> AutZinH isoGH isoGK defG eqZGHK; have [_ _ cGHK] := cprodP defG. have [|gz isoZ] := xcprodP. have [[fH injfH <-] [fK injfK <-]] := (isogP isoGH, isogP isoGK). rewrite -!injm_center -?(isog_transl _ (sub_isog _ _)) ?center_sub //=. by rewrite eqZGHK sub_isog ?center_sub. rewrite (isog_cprod_by _ defG) //. by apply/eqP; rewrite eqEsubset setIS // subsetI {2}eqZGHK !center_sub. 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)