chore: move test

Author: leodemoura

tests/lean/grind/omega_regressions.lean

@@ -1,9 +1,3 @@
 -- These are test cases extracted from Mathlib, where `omega` works but `grind` does not (yet!)
 
 example (n : Int) (n0 : ¬0 ≤ n) (a : Nat) : n ≠ (a : Int) := by grind
-
--- TODO: add to the library?
-attribute [grind] Int.negSucc_eq
-
-example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
-  (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by grind

tests/lean/run/grind_cutsat_eq_1.lean

@@ -69,3 +69,7 @@ example (a b : Int) : a = 0 → b = 1 → a + b > 2 → False := by
 
 example (a b c : Int) : a = 0 → a + b > 2 → b = c → 1 = c → False := by
   grind
+
+example (p : Int) (n : Nat) (hmp : Int.negSucc (n + 1) + 1 = p)
+    (hnm : Int.negSucc (n + 1 + 1) + 1 = Int.negSucc (n + 1)) : p = Int.negSucc n := by
+  grind