From de5352e64f36948fc568a1bbb58bf930ec44aa2c Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Mon, 25 Nov 2024 17:01:18 +0100
Subject: Day 13, Part 1

---
 Common/Nat.lean | 5 +++++
 1 file changed, 5 insertions(+)

(limited to 'Common')

diff --git a/Common/Nat.lean b/Common/Nat.lean
index a863a49..3a605a9 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -15,3 +15,8 @@ theorem two_d_coordinate_to_index_lt_size {x y w h: Nat} (h₁ : x < w) (h₂ :
 theorem gt_of_sub_lt {a b c : Nat} (h₁ : a - b < a - c) : c < b := by omega
 
 theorem sub_lt_of_gt {a b c : Nat} (h₁ : b ≤ a) (h₂ : c < b) : a - b < a - c := by omega
+
+theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) :=
+  match b with
+  | 0 => h₁
+  | _ + 1 => /-(Nat.pred_succ a).substr $-/ Nat.lt_succ_of_lt h₁
-- 
cgit v1.2.3