proposition: Lemma gFmod_cont : GFunctor.continuous (F1 %% F2).
proof: Proof. move=> gT rT G f; have nF2 := gFnorm F2. have sDF: G \subset 'dom (coset (F2 _ G)) by rewrite nF2. have sDFf: G \subset 'dom (coset (F2 _ (f @* G)) \o f). by rewrite -sub_morphim_pre ?subsetIl // nF2. pose K := 'ker (restrm sDFf (coset (F2 _ (f @* G)) \o f)). have sFK: 'ker (restrm sDF (coset (F2 _ G))) \subset K. rewrite {}/K !ker_restrm ker_comp /= subsetI subsetIl !ker_coset /=. by rewrite -sub_morphim_pre ?subsetIl // morphimIdom ?morphimF. have sOF := gFsub F1 (G / F2 _ G); have sGG: G \subset G by []. rewrite -sub_quotient_pre; last first. by apply: subset_trans (nF2 _ _); rewrite morphimS ?gFmod_closed. suffices im_fact H : F2 _ G \subset gval H -> H \subset G -> factm sFK sGG @* (H / F2 _ G) = f @* H / F2 _ (f @* G). - rewrite -2?im_fact ?gFmod_closed ?gFsub //. by rewrite cosetpreK morphimF /= ?morphim_restrm ?setIid. by rewrite -sub_quotient_pre ?normG //= trivg_quotient sub1G. move=> sFH sHG; rewrite -(morphimIdom _ (H / _)) /= {2}morphim_restrm setIid. rewrite -morphimIG ?ker_coset // -(morphim_restrm sDF) morphim_factm. by rewrite morphim_restrm morphim_comp -quotientE morphimIdom. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)