From 9c8021d0cd90fe6f0ed9a9c15679b80b099f4229 Mon Sep 17 00:00:00 2001
From: Andreas Grois <andi@grois.info>
Date: Thu, 8 Aug 2024 19:11:28 +0200
Subject: Minor

---
 BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
index a505c91..99ce68a 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean
@@ -816,10 +816,16 @@ case isFalse h₃ =>
       subst he6
       simp at he5
       subst rr2
+      subst oldValue
+      have : pp2+1+1 < o + (pp2 + 1 + 1) := by omega
+      have : ⟨j2 + 1 - o, by omega⟩ > (CompleteTree.Internal.heapRemoveLastWithIndex r).snd.snd := sorry
+      --have htest := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelationGt r ⟨j2 + 1 - o, by omega⟩ this
+      --simp at htest
       sorry
 case isTrue h₃ =>
   --removed left
   sorry
+--termination_by n
 
 protected theorem heapRemoveLastWithIndexRelation {α : Type u} {n : Nat} (heap : CompleteTree α (n+1)) (index : Fin (n+1)):
   let (result, removedElement, oldIndex) := CompleteTree.Internal.heapRemoveLastWithIndex heap
-- 
cgit v1.2.3