proposition: Lemma totientE n : n > 0 -> totient n = \prod_(p <- primes n) (p.-1 * p ^ (logn p n).-1).
proof: Proof. move=> n_gt0; rewrite /totient n_gt0 prime_decompE unlock. by elim: (primes n) => //= [p pr ->]; rewrite !natTrecE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)