proposition: Lemma totient_gt0 n : (0 < totient n) = (0 < n).
proof: Proof. case: n => // n; rewrite totientE // big_seq_cond prodn_cond_gt0 // => p. by rewrite mem_primes muln_gt0 expn_gt0; case: p => [|[|]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(fintype div bigop)