proposition: Lemma Aut_conj_aut A : conj_aut @* A \subset Aut G.
proof: Proof. by apply/subsetP=> _ /imsetP[x _ ->]; apply: Aut_aut. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)