proposition: Lemma sgvalmK A : subg G @* (sgval @* A) = A.
proof: Proof. apply/eqP; rewrite eqEcard !card_injm ?subsetT ?sgval_sub // leqnn andbT. rewrite -morphim_comp; apply/subsetP=> _ /morphimP[v _ Av ->] /=. by rewrite sgvalK. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup)