proposition: Lemma totient_gen : totient #[a] = #|[set x | generator <[a]> x]|.
proof: Proof. have [lea1 | lt1a] := leqP #[a] 1. rewrite /order card_le1_trivg // cards1 (@eq_card1 _ 1) // => x. by rewrite !inE -cycle_eq1 eq_sym. rewrite -(card_injm (injm_invm (injm_Zpm a))) /= ?im_Zpm; last first. by apply/subsetP=> x /[1!inE]; apply: cycle_generator. rewrite -card_units_Zp // cardsE card_sub morphim_invmE; apply: eq_card => /= d. by rewrite !inE /= qualifE /= /Zp lt1a inE /= generator_coprime {1}Zp_cast. 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)