feat: grind_pattern natCast_nonneg

[kim-em]

This PR adds a lemma that the cast of a natural number into any ordered ring is non-negative. We can't annotate this directly for grind, but will probably add this to grind's linarith interrnals.

[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 5326530383a4d0c65d4a8b008ae2327c491b25be --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-10 23:35:24)

[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 5326530383a4d0c65d4a8b008ae2327c491b25be --onto 19e1fe55f33a8aadc4243da32828b70a4b4677cc. You can force reference manual CI using the force-manual-ci label. (2025-12-10 23:35:26)