mathlib3

2609ad04 - chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203)

chore(data/nat/digits): golf, use seemingly weaker assumptions (#18203) * Golf. * Assume `n ≠ 0` instead of `0 < n` or `1 ≤ n`. * Assume `1 < n` instead of `2 ≤ n`. * Add `nat.exists_eq_add_of_le'` (forward-ported in leanprover-community/mathlib4#1662).