From 4848d2516919ab7e5652b20e2b33e7cc39a9d4d9 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 28 Nov 2024 21:53:47 +0100
Subject: Day 14, Part 1.

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

(limited to 'Common/Nat.lean')

diff --git a/Common/Nat.lean b/Common/Nat.lean
index 3a605a9..9d0ee29 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -20,3 +20,6 @@ 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₁
+
+theorem lt_imp_pred_lt {a b : Nat} (h₁ : a < b) : (a.pred < b) :=
+  Nat.lt_of_le_of_lt (Nat.pred_le a) h₁
-- 
cgit v1.2.3