mathlib

75bf5660 - feat(data/zmod): a lemma on `zmod.val_min_abs` on negations (#17584)

feat(data/zmod): a lemma on `zmod.val_min_abs` on negations (#17584) And two necessary lemmas about `nat`, courtesy of @kmill . Co-authored-by: Kyle Miller @kmill Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>