feat: more Nat range lemmas

[datokrat]

This PR provides specialized lemmas about Nat ranges, including simp annotations and induction principles for proving properties for all ranges.

[datokrat]

!radar

[leanprover-radar]

Benchmark results for b89b83c against 1ecda60 are in! @datokrat

Major changes (5)

• 🟥 build//instructions: +50.2G (+0.4%)
• 🟥 import Lean//instructions: +30.9M (+1.6%)
• 🟥 size/init/.olean.private//bytes: +2MiB (+0.8%)
• 🟥 size/init/.olean.server//bytes: +212kiB (+2.3%)
• 🟥 size/stdlib/.olean.server//bytes: +212kiB (+0.8%)

Minor changes (3)

• 🟥 size/init/.olean//bytes: +411kiB (+0.5%)
• 🟥 size/stdlib/.ilean//bytes: +193kiB (+0.3%)
• 🟥 size/stdlib/.lean//lines: +2.4k (+0.4%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fc6e0454c739313058b4eb209d64916023ced496 --onto 16508196e0dfa0702868333eecf6f6dc8b58d632. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 10:05:49)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase fc6e0454c739313058b4eb209d64916023ced496 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-01 11:38:42)
• ❌ Mathlib branch lean-pr-testing-11321 built against this PR, but testing failed. (2025-12-02 10:59:06) View Log
• ✅ Mathlib branch lean-pr-testing-11321 has successfully built against this PR. (2025-12-02 15:13:01) View Log

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase fc6e0454c739313058b4eb209d64916023ced496 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-01 10:05:51)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2025-12-01 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2025-12-02 09:58:00)