proposition: Lemma im_subg : subg G @* G = [subg G].
proof: Proof. apply/eqP; rewrite -subTset morphimEdom. by apply/subsetP=> u _; rewrite -(sgvalK u) imset_f ?subgP. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)