proposition: Lemma subgmK (A : {set gT}) : A \subset G -> sgval @* (subg G @* A) = A.
proof: Proof. move=> sAG; apply/eqP; rewrite eqEcard !card_injm ?subsetT //. rewrite leqnn andbT -morphim_comp morphimE /= morphpreT. by apply/subsetP=> _ /morphimP[v Gv Av ->] /=; rewrite subgK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)