proposition: Lemma totient_prime_alt n: 1 < n -> totient n = n.-1 -> prime n.
proof: Proof. move => n1; move:(ltnW n1) => n0. move:(pdiv_prime n1); set u := (pdiv n) => pu. move:(pfactor_coprime pu n0)(prime_gt1 pu) => [m pa pb] u1. have lp : 0 < logn u n by rewrite logn_gt0 mem_primes pu n0 pdiv_dvd. have pc: coprime m (u ^ logn u n) by rewrite coprime_sym; apply:coprimeXl. case m1: (m==1). set y := u.-1 * u ^ (logn u n).-1. have yp: 0 < y by rewrite muln_gt0 expn_gt0 -ltnS (ltnW u1) (ltn_predK u1) u1. rewrite pb (eqP m1) mul1n totient_pfactor// -{2 3}(prednK lp) expnS. rewrite - {4} (prednK (ltnW u1)) mulSn -/y -(prednK yp) addnS /=. by move/eqP; rewrite - add1n eqn_add2r=> /eqP <-; rewrite muln1. case: (posnP m)=> mz h; first by move: n0; rewrite pb mz ltnn. have /totient_ltn ha: 1 <m by rewrite ltn_neqAle eq_sym m1 mz. have /totient_ltn hb: 1 < (u ^ logn u n). by apply: (leq_trans u1); rewrite -{1} (expn1 u) leq_pexp2l // (ltnW u1). move: (leq_mul ha hb); rewrite mulSn mulnS addnA -(totient_coprime pc) - pb. rewrite h addSn addSnnS (prednK n0) - {3} (add0n n) leq_add2r leqn0 addn_eq0. by move: mz; rewrite - totient_gt0 => /gtn_eqF ->; rewrite andbF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)