From 8223584095273bc7bdf7b7dc65a6e168350cdf57 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sat, 14 Dec 2024 00:09:46 +0100
Subject: Begin Day16

---
 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 9d0ee29..bc66a09 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -23,3 +23,6 @@ theorem lt_of_pred_lt {a b : Nat} (h₁ : a < b.pred) : (a < b) :=
 
 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₁
+
+theorem le_of_add_le {a b c d : Nat} (h₁ : a ≤ b + c) (h₂ : c ≤ d) : a ≤ b + d :=
+  Nat.le_trans h₁ (Nat.add_le_add_left h₂ b)
-- 
cgit v1.2.3