chore: fix bug in omega

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

@@ -150,7 +150,7 @@ partial def groundInt? (e : Expr) : Option Int :=
     | _, _ => none
   | _ => e.int?
 where op (f : Int → Int → Int) (x y : Expr) : Option Int :=
-  match groundNat? x, groundNat? y with
+  match groundInt? x, groundInt? y with
     | some x', some y' => some (f x' y')
     | _, _ => none
 

tests/lean/run/omega.lean

@@ -382,6 +382,10 @@ example (x : Nat) : x < 2 →
     (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2) ∧ (0 = 0 → 0 = 0 → 0 = 0 → 0 = 0 → x < 2 → x < 3) := by
   omega
 
+-- Reported in Lean FRO office hours 2024-05-16 by Michael George
+example (s : Int) (s0 : s < (0 : Int)) : 63 + (s - 2 ^ 63) ≤ 62 - 2 ^ 63 := by
+  omega
+
 /-! ### Fin -/
 
 -- Test `<`