proposition: Lemma sum_ncycle_totient : \sum_(d < #|G|.+1) #|[set <[x]> | x in G & #[x] == d]| * totient d = #|G|.
proof: Proof. pose h (x : gT) : 'I_#|G|.+1 := inord #[x]. symmetry; rewrite -{1}sum1_card (partition_big h xpredT) //=. apply: eq_bigr => d _; set Gd := finset _. rewrite -sum_nat_const sum1dep_card -sum1_card (_ : finset _ = Gd); last first. apply/setP=> x /[!inE]; apply: andb_id2l => Gx. by rewrite /eq_op /= inordK // ltnS subset_leq_card ?cycle_subG. rewrite (partition_big_imset cycle) {}/Gd; apply: eq_bigr => C /=. case/imsetP=> x /setIdP[Gx /eqP <-] -> {C d}. rewrite sum1dep_card totient_gen; apply: eq_card => y; rewrite !inE /generator. move: Gx; rewrite andbC eq_sym -!cycle_subG /order. by case: eqP => // -> ->; rewrite eqxx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)