proposition: Lemma gFmod_closed : GFunctor.closed (F1 %% F2).
proof: Proof. by move=> gT G; rewrite sub_cosetpre_quo ?gFsub ?gFnormal. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)