proposition: Lemma totient_leq n : totient n <= n.
proof: Proof. rewrite totient_count_coprime. rewrite -{3}[n]muln1 -{3}[n]subn0 -sum_nat_const_nat. by apply: leq_sum => i _; case: coprime. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_field) mathcomp(ssralg finalg poly polydiv zmodp vector qpoly)