chore: incorrect lemma resolution in omega (#4141)

Fixes #4138.

src/Lean/Elab/Tactic/Omega/OmegaM.lean

@@ -199,7 +199,7 @@ def analyzeAtom (e : Expr) : OmegaM (HashSet Expr) := do
       | some _ =>
         let b_pos := mkApp4 (.const ``LT.lt [0]) (.const ``Int []) (.const ``Int.instLTInt [])
           (toExpr (0 : Int)) b
-        let pow_pos := mkApp3 (.const ``Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
+        let pow_pos := mkApp3 (.const ``Lean.Omega.Int.pos_pow_of_pos []) b exp (← mkDecideProof b_pos)
         pure <| HashSet.empty.insert
           (mkApp3 (.const ``Int.emod_nonneg []) x k
               (mkApp3 (.const ``Int.ne_of_gt []) k (toExpr (0 : Int)) pow_pos)) |>.insert

tests/lean/run/omega.lean

@@ -426,6 +426,10 @@ example (x e : Nat) (hx : x < 2^(e.succ)) : x < 2^e * 2 := by omega
 -- Check that this works for integer base.
 example (x : Int) (e : Nat) (hx : x < (2 : Int)^(e+1)) : x < 2^e * 2 := by omega
 
+example (n : Nat) (i : Int) (h2n : (2 : Int) ^ n = ↑((2 : Nat) ^ (n : Nat)))
+    (hlt : i % 2 ^ n < 2 ^ n) :  2 ^ n ≠ 0 := by
+  omega
+
 /-! ### Ground terms -/
 
 example : 2^7 < 165 := by omega