proposition: Lemma Aut_group_set : group_set (Aut G).
proof: Proof. apply/group_setP; split=> [|a b]. by rewrite inE perm_on1; apply/morphicP=> ? *; rewrite !permE. rewrite !inE => /andP[Ga aM] /andP[Gb bM]; rewrite perm_onM //=. apply/morphicP=> x y Gx Gy; rewrite !permM (morphicP aM) //. by rewrite (morphicP bM) ?perm_closed. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)