proposition: Lemma Aut1 : Aut 1 = 1.
proof: Proof. apply/trivgP/subsetP=> a /= AutGa; apply/set1P. apply: eq_Aut (AutGa) (group1 _) _ => _ /set1P->. by rewrite -(autmE AutGa) morph1 perm1. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)