proposition: Lemma eq_Aut A : {in Aut A &, forall a b, {in A, a =1 b} -> a = b}.
proof: Proof. move=> a g Aa Ag /= eqag; apply/permP=> x. by have [/eqag // | /out_Aut out] := boolP (x \in A); rewrite !out. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)