proposition: Lemma gFmod_hereditary : GFunctor.hereditary (F1 %% F2).
proof: Proof. move=> gT H G sHG; set FGH := _ :&: H; have nF2H := gFnorm F2 H. rewrite -sub_quotient_pre; last exact: subset_trans (subsetIr _ _) _. pose rH := restrm nF2H (coset (F2 _ H)); pose rHM := [morphism of rH]. have rnorm_simpl: rHM @* H = H / F2 _ H by rewrite morphim_restrm setIid. have nF2G := subset_trans sHG (gFnorm F2 G). pose rG := restrm nF2G (coset (F2 _ G)); pose rGM := [morphism of rG]. have sqKfK: 'ker rGM \subset 'ker rHM. rewrite !ker_restrm !ker_coset (setIidPr (gFsub F2 _)) setIC /=. exact: gFhereditary. have sHH := subxx H; rewrite -rnorm_simpl /= -(morphim_factm sqKfK sHH) /=. apply: subset_trans (gFcont F1 _); rewrite /= {2}morphim_restrm setIid /=. apply: subset_trans (morphimS _ (gFhereditary _ (quotientS _ sHG))) => /=. have ->: FGH / _ = restrm nF2H (coset _) @* FGH. by rewrite morphim_restrm setICA setIid. rewrite -(morphim_factm sqKfK sHH) morphimS //= morphim_restrm -quotientE. by rewrite setICA setIid (subset_trans (quotientI _ _ _)) // cosetpreK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)