proposition: Lemma idGfun_monotonic : GFunctor.monotonic idGfun.
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)