From 1ebf51d73981f521c70e5e30fd1bf19977cfb306 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 9 Dec 2023 21:21:09 +0100
Subject: Day9: Simplify proof of termination

---
 Day9.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Day9.lean b/Day9.lean
index 24cd19d..0d28d27 100644
--- a/Day9.lean
+++ b/Day9.lean
@@ -30,7 +30,7 @@ private def extrapolate : List Int → Int
   if a == 0 && as.all (· == 0) then
     0
   else
-    have : List.length (Day9.differences (a :: as)) < Nat.succ (List.length as) := by
+    have : (differences (a :: as)).length < as.length + 1 := by
       simp_arith[differences]
       induction (as) <;> simp_arith[differences]
       case cons b bs hb => rw[←differences_length_independent_arg]
-- 
cgit v1.2.3