proposition: Lemma gFcomp_cont : GFunctor.continuous (F1 \o F2).
proof: Proof. move=> gT rT G phi; rewrite (subset_trans (morphimF _ _ (gFsub _ _))) //. by rewrite (subset_trans (gFunctorS F1 (gFcont F2 phi))). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)