proposition: Lemma trivm_morphM (A : {set aT}) : {in A &, {morph trivm A : x y / x * y}}.
proof: Proof. by move=> x y /=; rewrite mulg1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)