proposition: Lemma trivGfun_cont : GFunctor.pcontinuous trivGfun.
proof: Proof. by move=> gT rT D G f; rewrite morphim1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(bigop finset fingroup morphism automorphism) mathcomp(quotient gproduct)