proposition: Lemma astab1JG G : 'C[G | 'JG] = 'N(G).
proof: Proof. by apply/setP=> x; apply/astab1P/normP=> [/congr_group | /group_inj]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)