proposition: Lemma class_formula : \sum_(C in classes G) #|G : 'C_G[repr C]| = #|G|.
proof: Proof. rewrite -sum_card_class; apply: eq_bigr => _ /imsetP[x Gx ->]. have: x \in x ^: G by rewrite -{1}(conjg1 x) imset_f. by case/mem_repr/imsetP=> y Gy ->; rewrite index_cent1 classGidl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat div seq) mathcomp(fintype bigop finset fingroup morphism perm) mathcomp(automorphism quotient)