proposition: Lemma totient_prime p : prime p -> totient p = p.-1.
proof: Proof. by move=> p_prime; rewrite -{1}[p]expn1 totient_pfactor // muln1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)