proposition: Lemma totient_ltn n: 1 < n -> totient n < n.
proof: Proof. move => l1n; rewrite totient_count_coprime. rewrite -{1 3}(prednK (ltnW l1n)) big_nat_recl // /coprime gcdn0 (gtn_eqF l1n). move:(sum_nat_const_nat 0 n.-1 1); rewrite subn0 muln1 => {2} <-. by rewrite ltnS; apply: 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)