proposition: Lemma totient_prime n: prime n = (0 < n) && (totient n == n.-1).
proof: Proof. case: (posnP n) => np /=; first by rewrite np. case pn:(prime n); first by rewrite -{1}(expn1 n) totient_pfactor // muln1 eqxx. case/primePn: (negbT pn). by rewrite ltnS leqn1; case/orP => /eqP => h; move: np; rewrite h. move => [d /andP[l1d ldn] /gcdn_idPr gnd]. symmetry; apply: ltn_eqF. have ns:= prednK np; have dc:= (prednK(ltnW l1d)). have df: d.-1 < n.-1 by rewrite -ltnS dc ns. rewrite totient_count_coprime -{1}ns big_nat_recl // {1} /coprime gcdn0. rewrite (gtn_eqF (ltn_trans l1d ldn)). rewrite -{2} (card_ord n.-1) - sum1_card big_mkord. rewrite (bigD1 (Ordinal df)) // [X in _ < X] (bigD1 (Ordinal df)) //=. rewrite dc /coprime gnd (gtn_eqF l1d) 2!add0n add1n ltnS. by rewrite leq_sum // => i _; case: eqP. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)