proposition: Lemma conj_autE : {in G &, forall x y, conj_aut x y = y ^ x}.
proof: Proof. by apply: sub_in11 norm_conj_autE => //; apply: subsetP (normG G). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)