mathlib3

3ed3f98a - feat(data/nat/order/basic): `a + b - 1 ≤ a * b` (#18737)

feat(data/nat/order/basic): `a + b - 1 ≤ a * b` (#18737) and golf `max_eq_zero_iff`/`min_eq_zero_iff` To be used for Kneser's addition theorem. Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>