proposition: Lemma astabJ A : 'C(A |'J) = 'C(A).
proof: Proof. apply/setP=> x; apply/astabP/centP=> cAx y Ay /=. by apply: esym; rewrite 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)