proposition: Lemma card_classes_abelian : abelian G = (#|classes G| == #|G|).
proof: Proof. have cGgt0 C: C \in classes G -> 1 <= #|C| ?= iff (#|C| == 1)%N. by case/imsetP=> x _ ->; rewrite eq_sym -index_cent1. rewrite -sum_card_class -sum1_card (leqif_sum cGgt0). apply/abelian_classP/forall_inP=> [cGG _ /imsetP[x Gx ->]| cGG x Gx]. by rewrite cGG ?cards1. apply/esym/eqP; rewrite eqEcard sub1set cards1 class_refl leq_eqVlt cGG //. exact: imset_f. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)