mathlib

bfa40102 - feat(data/nat/modeq): `modeq.le_of_lt_add` (#9816)

feat(data/nat/modeq): `modeq.le_of_lt_add` (#9816) If `a ≡ b [MOD m]` and `a < b + m`, then `a ≤ b`. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>