mathlib3

feat(data/zmod): lemmas about totient and zmod

#2158

Merged