proposition: Lemma gFunctorS (F : GFunctor.mono_map) : GFunctor.monotonic F.
proof: Proof. by case: F. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)