proposition: Lemma ker_conj_aut : 'ker conj_aut = 'C(G).
proof: Proof. apply/setP=> x /[1!inE]; case nGx: (x \in 'N(G)); last first. by symmetry; apply/idP=> cGx; rewrite (subsetP (cent_sub G)) in nGx. rewrite 2!inE /=; apply/eqP/centP=> [cx1 y Gy | cGx]. by rewrite /commute (conjgC y) -norm_conj_autE // cx1 perm1. apply/permP=> y; case Gy: (y \in G); last by rewrite !permE Gy. by rewrite perm1 norm_conj_autE // conjgE -cGx ?mulKg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat fintype) mathcomp(finset fingroup perm morphism)