proposition: Lemma morphim_groupset G : group_set (f @* G).
proof: Proof. apply/group_setP; split=> [|_ _ /morphimP[x Dx Gx ->] /morphimP[y Dy Gy ->]]. by rewrite -morph1 imset_f ?group1. by rewrite -morphM ?imset_f ?inE ?groupM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)