proposition: Lemma afixJG G A : (G \in 'Fix_('JG)(A)) = (A \subset 'N(G)).
proof: Proof. by apply/afixP/normsP=> nG x Ax; apply/eqP; move/eqP: (nG x Ax). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)