proposition: Lemma abelian_classP : reflect {in G, forall x, x ^: G = [set x]} (abelian G).
proof: Proof. rewrite /abelian -astabJ astabC. by apply: (iffP subsetP) => cGG x Gx; apply/orbit1P; apply: cGG. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)