Commit 2023-12-26 11:03 10597c9e

feat: Lemmas about ZMod (#9143) Added some lemmas about ZMod and its units:

• Generalized lt to le in two lemmas
• ((a : ZMod n) : ZMod m) = a if m ≤ n
• unitsMap is surjective
• Units.map f (-a) = -Units.map f a (which can be applied to unitsMap)
• Units.map (-1) = -1 (which can be applied to unitsMap)