proposition: Lemma totient_pfactor_alt p e: prime p -> 0 < e -> totient (p ^ e) = p ^ e - p ^ e.-1.
proof: Proof. move => pp ep; rewrite totient_pfactor // -{2} (prednK ep) expnS. by rewrite - {3} (prednK (prime_gt0 pp)) mulSn addKn. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)