From 97e8285eaaacf54fd3689fc2862a1faea81694dd Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 30 Jun 2024 20:58:59 +0200
Subject: Finish CompleteTree.get implementation. Not proven to be correct yet.

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

(limited to 'Common/Nat.lean')

diff --git a/Common/Nat.lean b/Common/Nat.lean
index 1721653..0a0f1f4 100644
--- a/Common/Nat.lean
+++ b/Common/Nat.lean
@@ -166,3 +166,11 @@ theorem Nat.sub_lt_of_lt_add {a b c : Nat} (h₁ : a < c + b) (h₂ : b ≤ a) :
   have h₇ : 1 + (a-b) ≤ c := h₆.subst (motive := λx ↦ x ≤ c) h₅
   have h₈ : (a-b) + 1 ≤ c := (Nat.add_comm 1 (a-b)).subst (motive := λx ↦ x ≤ c) h₇
   Nat.lt_of_succ_le h₈
+
+theorem Nat.sub_lt_sub_right {a b c : Nat} (h₁ : b ≤ a) (h₂ : a < c) : (a - b < c - b) := by
+  apply Nat.sub_lt_of_lt_add
+  case h₂ => assumption
+  case h₁ =>
+    have h₃ : b ≤ c := Nat.le_of_lt $ Nat.lt_of_le_of_lt h₁ h₂
+    rw[Nat.sub_add_cancel h₃]
+    assumption
-- 
cgit v1.2.3