From 65a77968d0abc2d01da92aa8982256855e7519a6 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Fri, 5 Apr 2024 14:04:25 +0200
Subject: Update the lean toolchain and fix the proofs

---
 backends/lean/Base/Diverge/Base.lean | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'backends/lean/Base/Diverge/Base.lean')

diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index e40432bd..7521eecc 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -1,7 +1,6 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Mathlib.Tactic.RunCmd
 import Mathlib.Tactic.Linarith
 import Base.Primitives.Base
 import Base.Arith.Base
@@ -39,8 +38,7 @@ namespace Lemmas
     case zero =>
       simp_all
       intro m h1 h2
-      have h: n = m := by
-        linarith
+      have h: n = m := by omega
       unfold for_all_fin_aux; simp_all
       simp_all
       -- There is no i s.t. m ≤ i
-- 
cgit v1.2.3