proposition: Lemma afixJ A : 'Fix_('J)(A) = 'C(A).
proof: Proof. apply/setP=> x; apply/afixP/centP=> cAx y Ay /=. by rewrite /commute conjgC cAx. by rewrite conjgE cAx ?mulKg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)