mathlib3

7a89b1ae - feat(data/int/cast/lemmas): `a.nat_mod b < b` (#17896)

feat(data/int/cast/lemmas): `a.nat_mod b < b` (#17896) The modulus of an integer by a natural is strictly less than the natural. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>