From 7a51fa8ec50406cc770baac2d83d47e2607ad9a2 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Thu, 21 Dec 2023 18:25:40 +1100
Subject: [PATCH] feat: omega supports Nat.succ (#474)

---
 Std/Tactic/Omega/Frontend.lean | 1 +
 test/omega/test.lean           | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/Std/Tactic/Omega/Frontend.lean b/Std/Tactic/Omega/Frontend.lean
index a4457bec20..227f622767 100644
--- a/Std/Tactic/Omega/Frontend.lean
+++ b/Std/Tactic/Omega/Frontend.lean
@@ -179,6 +179,7 @@ partial def asLinearComboImpl (e : Expr) : OmegaM (LinearCombo × OmegaM Expr ×
         mkAtomLinearCombo e
     | _ => mkAtomLinearCombo e
   | (``Nat.cast, #[_, _, n]) => match n.getAppFnArgs with
+    | (``Nat.succ, #[n]) => rewrite e (.app (.const ``Int.ofNat_succ []) n)
     | (``HAdd.hAdd, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_add []) a b)
     | (``HMul.hMul, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_mul []) a b)
     | (``HDiv.hDiv, #[_, _, _, _, a, b]) => rewrite e (mkApp2 (.const ``Int.ofNat_ediv []) a b)
diff --git a/test/omega/test.lean b/test/omega/test.lean
index f1a83735b0..e7dbd6d9a5 100644
--- a/test/omega/test.lean
+++ b/test/omega/test.lean
@@ -26,6 +26,8 @@ example {x : Int} : x / 0 = 0 := by omega
 
 example {x : Int} : x / 2 + x / (-2) = 0 := by omega
 
+example {x y z : Nat} (_ : a ≤ c) (_ : b ≤ c) : a < Nat.succ c := by omega
+
 example (_ : 7 < 3) : False := by omega
 example (_ : 0 < 0) : False := by omega