feat: add instances NeZero(n^0) for n : Nat and n : Int

[fgdorais]

This PR adds two missing NeZero instances for n^0 where n : Nat and n : Int.

---

Note

Add NeZero instances for n^0 when n : Nat and n : Int.

^{Written by Cursor Bugbot for commit 8305e65. This will update automatically on new commits. Configure here.}

[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 a73ebe8a772be4aa99e7f10e6be2443211340d90 --onto 705dac4f77aa60d749ee2b37d102518d772d6e53. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-10 21:38:49)

[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 a73ebe8a772be4aa99e7f10e6be2443211340d90 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-10 21:38:51)

[fgdorais]

Forward port at batteries#1455.