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

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

<!-- CURSOR_SUMMARY -->
---

> [!NOTE]
> Add NeZero instances for n^0 when n : Nat and n : Int.
> 
> <sup>Written by [Cursor
Bugbot](https://cursor.com/dashboard?tab=bugbot) for commit
8305e65ba5d7037a6b1f5a631596822709f48c0a. This will update automatically
on new commits. Configure
[here](https://cursor.com/dashboard?tab=bugbot).</sup>
<!-- /CURSOR_SUMMARY -->

Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

src/Init/Data/Int/Pow.lean

@@ -62,6 +62,8 @@ protected theorem pow_ne_zero {n : Int} {m : Nat} : n ≠ 0 → n ^ m ≠ 0 := b
 
 instance {n : Int} {m : Nat} [NeZero n] : NeZero (n ^ m) := ⟨Int.pow_ne_zero (NeZero.ne _)⟩
 
+instance {n : Int} : NeZero (n^0) := ⟨Int.one_ne_zero⟩
+
 @[simp, norm_cast]
 protected theorem natCast_pow (b n : Nat) : ((b^n : Nat) : Int) = (b : Int) ^ n := by
   match n with

src/Init/Data/Nat/Basic.lean

@@ -817,6 +817,8 @@ protected theorem two_pow_pos (w : Nat) : 0 < 2^w := Nat.pow_pos (by decide)
 instance {n m : Nat} [NeZero n] : NeZero (n^m) :=
   ⟨Nat.ne_zero_iff_zero_lt.mpr (Nat.pow_pos (pos_of_neZero _))⟩
 
+instance {n : Nat} : NeZero (n^0) := ⟨Nat.one_ne_zero⟩
+
 protected theorem mul_pow (a b n : Nat) : (a * b) ^ n = a ^ n * b ^ n := by
   induction n with
   | zero => simp [Nat.pow_zero]