proposition: Lemma gFcompS : GFunctor.monotonic (F1 \o F2).
proof: Proof. by move=> gT H G sHG; rewrite !gFunctorS. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)