proposition: Lemma snd_morphM : {morph (@snd gT1 gT2) : x y / x * y}.
proof: Proof. by move=> x y. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)