From d53610ae89d3da780b9beee52c8bfe88f45d5826 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Sun, 4 Aug 2024 12:40:29 +0200
Subject: Continue heapUpdateRootOnlyUpdatesRoot

---
 .../CompleteTree/AdditionalProofs/HeapUpdateRoot.lean       | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
index 3333f1f..71accaa 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapUpdateRoot.lean
@@ -108,5 +108,16 @@ theorem heapUpdateRootOnlyUpdatesRoot {α : Type u} {n : Nat} (le : α → α 
         else
           -- index was in r
           simp only [h, ↓reduceDite] at h₃
-          sorry
+          split
+          case isTrue h₄ _ _ _ _ _ =>
+            simp
+            rw[contains_as_root_left_right _ _ (Nat.succ_pos _)]
+            right
+            right
+            rw[←h₃, contains_iff_index_exists', right_unfold]
+            have h₄ : j < oo + 1 + (pp + 1) := Nat.lt_of_succ_lt_succ h₄
+            have : oo + 1 ≤ j := Nat.le_of_not_gt h
+            have : j - (oo + 1) < pp + 1 := Nat.sub_lt_left_of_lt_add this h₄
+            exists ⟨j-(oo+1), this⟩
+          case isFalse => sorry
 termination_by n
-- 
cgit v1.2.3