chore(data/nat/totient): golf three lemmas (#13886)
chore(data/nat/totient): golf three lemmas (#13886)

Golf the proofs of `totient_le`, `totient_lt`, and `totient_pos`





leanprover-community/mathlib,leanprover-community/mathlib