proposition: Lemma factm_morphM : {in q @* G &, {morph ff : x y / x * y}}.
proof: Proof. move=> _ _ /morphimP[x Hx Gx ->] /morphimP[y Hy Gy ->]. by rewrite -morphM ?factmE ?groupM // morphM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)