proposition: Lemma sum_totient_dvd n : \sum_(d < n.+1 | d %| n) totient d = n.
proof: Proof. case: n => [|[|n']]; try by rewrite big_mkcond !big_ord_recl big_ord0. set n := n'.+2; pose x1 : 'Z_n := 1%R. have ox1: #[x1] = n by rewrite /order -Zp_cycle card_Zp. rewrite -[rhs in _ = rhs]ox1 -[#[_]]sum_ncycle_totient [#|_|]ox1 big_mkcond /=. apply: eq_bigr => d _; rewrite -{2}ox1; case: ifP => [|ndv_dG]; last first. rewrite eq_card0 // => C; apply/imsetP=> [[x /setIdP[Gx oxd] _{C}]]. by rewrite -(eqP oxd) order_dvdG in ndv_dG. move/cycle_sub_group; set Gd := [set _] => def_Gd. rewrite (_ : _ @: _ = @gval _ @: Gd); first by rewrite imset_set1 cards1 mul1n. apply/setP=> C; apply/idP/imsetP=> [| [gC GdC ->{C}]]. case/imsetP=> x /setIdP[_ oxd] ->; exists <[x]>%G => //. by rewrite -def_Gd inE -Zp_cycle subsetT. have:= GdC; rewrite -def_Gd => /setIdP[_ /eqP <-]. by rewrite (set1P GdC) /= imset_f // inE eqxx (mem_cycle x1). 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)