mathlib3

4df649cb - feat(data/nat/modeq): Upper bound for `chinese_remainder` (#9783)

feat(data/nat/modeq): Upper bound for `chinese_remainder` (#9783) Proves that `chinese_remainder' < lcm n m` and `chinese_remainder < n * m`, as claimed by the doc-strings.