proposition: Lemma comp_morphM : {in f @*^-1 H &, {morph gof: x y / x * y}}.
proof: Proof. by move=> x y; rewrite /= !inE => /andP[? ?] /andP[? ?]; rewrite !morphM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)