proposition: Lemma totient_gt1 n : (totient n > 1)%N = (n > 2)%N.
proof: Proof. case: n => [|[|[|[|n']]]]//=; set n := n'.+4; rewrite [RHS]isT. have [pn2|/allPn[p]] := altP (@allP _ (eq_op^~ 2%N) (primes n)); last first. rewrite mem_primes/=; move: p => [|[|[|p']]]//; set p := p'.+3. move=> /andP[p_prime dvdkn]. have [//|[|k]// cpk ->] := (@pfactor_coprime _ n p_prime). rewrite totient_coprime ?coprimeXr 1?coprime_sym//. rewrite totient_pfactor ?logn_gt0 ?mem_primes ?p_prime// mulnCA. by rewrite (@leq_trans p.-1) ?leq_pmulr ?muln_gt0 ?expn_gt0 ?totient_gt0. have pnNnil : primes n != [::]. apply: contraTneq isT => pn0. by have := @prod_prime_decomp n isT; rewrite prime_decompE pn0/= big_nil. have := @prod_prime_decomp n isT; rewrite prime_decompE. case: (primes n) pnNnil pn2 (primes_uniq n) => [|p [|p' r]]//=; last first. move=> _ eq2; rewrite !inE [p](eqP (eq2 _ _)) ?inE ?eqxx//. by rewrite [p'](eqP (eq2 _ _)) ?inE ?eqxx// orbT. move=> _ /(_ _ (mem_head _ _))/eqP-> _; rewrite big_cons big_nil muln1/=. case: (logn 2 n) => [|[|k]]// ->. by rewrite totient_pfactor//= expnS mul1n leq_pmulr ?expn_gt0. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)