mathlib

e1192f35 - feat(data/nat/basic): add `mod_add_mod` and `add_mod_mod` (#2635)

feat(data/nat/basic): add `mod_add_mod` and `add_mod_mod` (#2635) Added the `mod_add_mod` and `add_mod_mod` lemmas for `data.nat.basic`. I copied them from `data.int.basic`, and just changed the data type. Would there be issues with it being labelled `@[simp]`? Also, would it make sense to refactor `add_mod` above it to use `mod_add_mod` and `add_mod_mod`? It'd make it considerably shorter. (Tangential note, there's a disparity between the `mod` lemmas for `nat` and the `mod` lemmas for `int`, for example `int` doesn't have `add_mod`, should that be added in a separate PR?)