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