proposition: Lemma injm_xcprodm : 'injm xcprodm = 'injm fH && 'injm fK.
proof: Proof. rewrite injm_cprodm !ker_ifactm !subG1 !morphim_injm_eq1 ?subsetIl // -!subG1. apply: andb_id2l => /= injfH; apply: andb_idr => _. rewrite !im_ifactm // -(morphimIdom gH) setI_im_cpair -injm_center //. rewrite morphim_ifactm // eqEsubset subsetI morphimS //=. rewrite {1}injm_center // setIS //=. rewrite (eq_in_morphim _ eq_fHK); first by rewrite morphim_comp morphimS. by rewrite !(setIidPr _) // -sub_morphim_pre. 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)