`omega` failing due to powers of numerals

Prerequisites

Please put an X between the brackets as you perform the following steps:

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies on Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to “Lean nightly”)

Description

The following example fails:

example (n : Nat) : 0 ≤ 2 ^ n := by 
  omega

with the message:

omega could not prove the goal:
a possible counterexample may satisfy the constraints
  a ≤ -1
where
 a := ↑2 ^ n

At the same time, the following more general example works:

example (m n : Nat) : 0 ≤ m ^ n := by 
  omega

Context

Related discussion in Zulip: #lean4 > Omega failing due to terms with power?

Steps to Reproduce

Run the code above.

Expected behavior: omega closes the goal above.

Actual behavior: omega fails to close the goal.

Versions

4.22.0-rc3
4.23.0-nightly-2025-07-04

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Start by running the minimal omega examples from the issue and compare the failing numeral-base power case with the working general case. Trace the omega implementation from its tactic entry point; done means the first example is closed while the existing general case continues to work.