Add a bunch of helper functions. Improve function signatures.

After using this in an actual program, I noticed some missing features,
like a helper to convert a list to a heap, or a way to fold over the
heap's values.

In addition, the BinaryHeap.pop function signature had a confusing order
of outputs.

9 files changed, 179 insertions, 101 deletions

diff --git a/BinaryHeap.lean b/BinaryHeap.lean
index 4f52f23..64dc552 100644
--- a/BinaryHeap.lean
+++ b/BinaryHeap.lean
@@ -1,85 +1,3 @@
-/-
-  This file contains the Binary Heap type and its basic operations.
--/
-import BinaryHeap.CompleteTree
-
-structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where
-  tree : BinaryHeap.CompleteTree α n
-  valid : BinaryHeap.HeapPredicate tree le
-  wellDefinedLe : BinaryHeap.transitive_le le ∧ BinaryHeap.total_le le
-deriving Repr
-
-namespace BinaryHeap
-
-/-- Creates an empty heap. O(1) -/
-def new (α : Type u) {le : α → α → Bool} (h₁ : transitive_le le) (h₂ : total_le le) : BinaryHeap α le 0 :=
-  {
-    tree := CompleteTree.empty,
-    valid := CompleteTree.emptyIsHeap le
-    wellDefinedLe := ⟨h₁,h₂⟩
-  }
-
-/-- Adds an element into a heap. O(log(n)) -/
-def push {α : Type u} {le : α → α → Bool} {n : Nat} : α → BinaryHeap α le n → BinaryHeap α le (n+1)
-| elem, .mk tree valid wellDefinedLe =>
-  let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right
-  let tree := tree.heapPush le elem
-  {tree, valid, wellDefinedLe}
-
-/-- Removes the smallest element from the heap and returns it. O(log(n)) -/
-def pop {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (BinaryHeap α le n × α)
-| {tree, valid, wellDefinedLe} =>
-  let result := tree.heapPop le
-  let resultValid := CompleteTree.heapPopIsHeap le tree valid wellDefinedLe
-  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
-
-/-- Removes the element at the given (depth-first) index from the heap and returns it. O(log(n)) -/
-def removeAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → (BinaryHeap α le n × α)
-| {tree, valid, wellDefinedLe}, index =>
-  let result := tree.heapRemoveAt le index
-  let resultValid := CompleteTree.heapRemoveAtIsHeap le index tree valid wellDefinedLe
-  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
-
-/-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/
-def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α)
-| {tree, valid, wellDefinedLe}, index, value =>
-  let result := tree.heapUpdateAt le index value
-  let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right
-  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
-
-/-- Searches for an element in the heap and returns its index. **O(n)** -/
-def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n)
-| {tree, valid := _, wellDefinedLe := _}, pred =>
-  tree.indexOf pred
-
-instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where
-  getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩
-
-instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where
-  getElem := λ heap index _ ↦ heap.tree.get index
-
-def forM [Monad m] (heap : BinaryHeap α le n) (f : α → m PUnit) : m PUnit :=
-  match n with
-  | .zero => pure ()
-  | .succ _ =>
-    let a := heap.tree.root' --this is faster than pop here, in case of a break.
-    f a >>= λ _ ↦ heap.pop.fst.forM f
-
-instance : ForM m (BinaryHeap α le n) α where
-  forM := BinaryHeap.forM
-
-instance : ForIn m (BinaryHeap α le n) α where
-  forIn := ForM.forIn
-
-/--Helper for the common case of using natural numbers for sorting.-/
-theorem nat_ble_to_heap_le_total : total_le Nat.ble :=
-  λa b ↦ Nat.ble_eq.substr $ Nat.ble_eq.substr (Nat.le_total a b)
-
-/--Helper for the common case of using natural numbers for sorting.-/
-theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble :=
-  λ a b c ↦
-    Nat.le_trans (n := a) (m := b) (k := c)
-    |> Nat.ble_eq.substr
-    |> Nat.ble_eq.substr
-    |> Nat.ble_eq.substr
-    |> and_imp.mpr
+import BinaryHeap.Basic
+import BinaryHeap.Aux
+import BinaryHeap.Relations
diff --git a/BinaryHeap/Aux.lean b/BinaryHeap/Aux.lean
new file mode 100644
index 0000000..0aa052d
--- /dev/null
+++ b/BinaryHeap/Aux.lean
@@ -0,0 +1,78 @@
+/-
+  This file contains some additional functions for a Binary Heap. Things that deal with
+  converting collections to/from a heap.
+-/
+import BinaryHeap.Basic
+
+namespace BinaryHeap
+
+def forM [Monad m] (heap : BinaryHeap α le n) (f : α → m PUnit) : m PUnit :=
+  match n with
+  | .zero => pure ()
+  | .succ _ =>
+    let a := heap.tree.root' --this is faster than pop here, in case of a break.
+    f a >>= λ _ ↦ heap.pop.snd.forM f
+
+instance : ForM m (BinaryHeap α le n) α where
+  forM := BinaryHeap.forM
+
+instance : ForIn m (BinaryHeap α le n) α where
+  forIn := ForM.forIn
+
+/-- Builds a Binary Heap from a list. -/
+def ofList {α : Type u} {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (l : List α) : BinaryHeap α le l.length :=
+  let rec worker : (l : List α) → {n : Nat} → (BinaryHeap α le n) → (BinaryHeap α le (n + l.length)) := λ (l : List α) {n : Nat} (heap : BinaryHeap α le n) ↦
+    match l with
+    | [] => heap
+    | a :: as => (Nat.add_comm_right n as.length 1).subst rfl ▸ worker as (heap.push a)
+  Nat.zero_add l.length ▸ worker l $ BinaryHeap.new h₁
+
+/- Converts the tree to a sorted list. -/
+def toList (heap : BinaryHeap α le n) : List α :=
+  let rec worker : (l : List α) → {n : Nat} → (BinaryHeap α le n) → List α := λ(l : List α) {n : Nat} (heap : BinaryHeap α le n) ↦
+    match n with
+    | 0 => l.reverse
+    | (_+1) =>
+      let (h, hs) := heap.pop
+      worker (h :: l) hs
+  worker [] heap
+
+private def ofForInAux [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : (h : Nat) ×' BinaryHeap α le h := Id.run do
+  let mut r : (h : Nat) ×' BinaryHeap α le h := ⟨0, BinaryHeap.new h₁⟩
+  for e in c do
+    r := ⟨r.fst.succ, r.snd.push e⟩
+  r
+
+/--
+  Runs a for-loop over the input collection and creates a heap from it.
+  Warning: Only terminates if the ForIn instance you call it with terminates.
+  Think of this as a "this doesn't depend on mathlib" alternative to an implementation that uses Traversable
+-/
+def ofForIn [ForIn Id ρ α] {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) (c : ρ) : BinaryHeap α le (ofForInAux h₁ c).fst := PSigma.snd $ ofForInAux h₁ c
+
+/--
+  Folds over the heap, starting at the smallest element and yielding the elements in ascending order.
+-/
+def fold (f : α → β → α) (init : α) (heap : BinaryHeap β le n) : α :=
+  match n with
+  | 0 => init
+  | (_+1) =>
+    let (a, as) := heap.pop
+    as.fold f (f init a)
+
+/--
+  Map operation over the heap.
+  Unlike the regular map operation, this requires you to supply a new ordering relation for the result type.
+  Needs to create a new heap with the mapped values.
+-/
+def map {α : Type u} {le₀ : α → α → Bool } {β : Type u₁} {le : β → β → Bool} (h₁ : TotalAndTransitiveLe le) (f : α → β) : (h : BinaryHeap α le₀ n) →  BinaryHeap β le n
+  | { tree, .. } =>
+    -- no need to do this in-order.
+    let rec worker : (o p : Nat) → (CompleteTree α o) → (BinaryHeap β le p) → (BinaryHeap β le (p + o)) := λ o p t h ↦
+      match o, t with
+      | 0, .leaf => h
+      | (q+r+1), .branch v left right _ _ _ =>
+        let left_result := worker q p left h
+        let right_result := worker r (p+q) right left_result
+        (Nat.add_assoc _ _ _▸right_result).push (f v)
+    (Nat.zero_add _)▸worker n 0 tree $ BinaryHeap.new h₁
diff --git a/BinaryHeap/Basic.lean b/BinaryHeap/Basic.lean
new file mode 100644
index 0000000..3f4a1f1
--- /dev/null
+++ b/BinaryHeap/Basic.lean
@@ -0,0 +1,61 @@
+/-
+  This file contains the Binary Heap type and its basic operations.
+-/
+import BinaryHeap.CompleteTree
+
+abbrev BinaryHeap.TotalAndTransitiveLe (le : α → α → Bool) : Prop := BinaryHeap.transitive_le le ∧ BinaryHeap.total_le le
+
+structure BinaryHeap (α : Type u) (le : α → α → Bool) (n : Nat) where
+  tree : BinaryHeap.CompleteTree α n
+  valid : BinaryHeap.HeapPredicate tree le
+  wellDefinedLe : BinaryHeap.TotalAndTransitiveLe le
+deriving Repr
+
+namespace BinaryHeap
+
+/-- Creates an empty heap. O(1) -/
+def new {α : Type u} {le : α → α → Bool} (h₁ : TotalAndTransitiveLe le) : BinaryHeap α le 0 :=
+  {
+    tree := CompleteTree.empty,
+    valid := CompleteTree.emptyIsHeap le
+    wellDefinedLe := h₁
+  }
+
+/-- Adds an element into a heap. O(log(n)) -/
+def push {α : Type u} {le : α → α → Bool} {n : Nat} : α → BinaryHeap α le n → BinaryHeap α le (n+1)
+| elem, .mk tree valid wellDefinedLe =>
+  let valid := tree.heapPushIsHeap valid wellDefinedLe.left wellDefinedLe.right
+  let tree := tree.heapPush le elem
+  {tree, valid, wellDefinedLe}
+
+/-- Removes the smallest element from the heap and returns it. O(log(n)) -/
+def pop {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (α × BinaryHeap α le n)
+| {tree, valid, wellDefinedLe} =>
+  let result := tree.heapPop le
+  let resultValid := CompleteTree.heapPopIsHeap le tree valid wellDefinedLe
+  (result.fst, { tree := result.snd, valid := resultValid, wellDefinedLe})
+
+/-- Removes the element at the given (depth-first) index from the heap and returns it. O(log(n)) -/
+def removeAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le (n+1)) → (Fin (n+1)) → (α × BinaryHeap α le n)
+| {tree, valid, wellDefinedLe}, index =>
+  let result := tree.heapRemoveAt le index
+  let resultValid := CompleteTree.heapRemoveAtIsHeap le index tree valid wellDefinedLe
+  (result.fst, { tree := result.snd, valid := resultValid, wellDefinedLe})
+
+/-- Updates the element at the given (depth-first) index and returns its previous value. O(log(n)) -/
+def updateAt {α : Type u} {le : α → α → Bool} {n : Nat} : (BinaryHeap α le n) → (Fin n) → α → (BinaryHeap α le n × α)
+| {tree, valid, wellDefinedLe}, index, value =>
+  let result := tree.heapUpdateAt le index value
+  let resultValid := CompleteTree.heapUpdateAtIsHeap le index value tree valid wellDefinedLe.left wellDefinedLe.right
+  ({ tree := result.fst, valid := resultValid, wellDefinedLe}, result.snd)
+
+/-- Searches for an element in the heap and returns its index. **O(n)** -/
+def indexOf {α : Type u} {le : α → α → Bool} {n : Nat} : BinaryHeap α le n → (pred : α → Bool) → Option (Fin n)
+| {tree, valid := _, wellDefinedLe := _}, pred =>
+  tree.indexOf pred
+
+instance : GetElem (BinaryHeap α le n) (Nat) α (λ _ index ↦ index < n) where
+  getElem := λ heap index h₁ ↦ heap.tree.get ⟨index, h₁⟩
+
+instance : GetElem (BinaryHeap α le n) (Fin n) α (λ _ _ ↦ True) where
+  getElem := λ heap index _ ↦ heap.tree.get index
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
index 09b1450..0fc88df 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapPop.lean
@@ -4,7 +4,7 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapUpdateRoot
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
-theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le : α → α → Bool) : (tree.heapPop le).snd = tree.root (Nat.succ_pos n) := by
+theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le : α → α → Bool) : (tree.heapPop le).fst = tree.root (Nat.succ_pos n) := by
   unfold heapPop
   split
   <;> simp only
@@ -22,14 +22,14 @@ theorem heapPopReturnsRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)
   case isTrue h₁ =>
     have h₂ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexLeavesRoot tree h₁
     have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameTree tree
-    simp only [h₃, heapUpdateRootReturnsRoot, h₂]
+    simp only [heapPop.Prod.swap, h₃, heapUpdateRootReturnsRoot, h₂]
 
 /--
   Shows that each element contained before removing the root that is not the root is still contained after removing the root.
   This is not a rigorous proof that the rest of the tree remained unchanged, as (1 (1 (1 1)) (2)).heapPop = (1 (2 (2 _)) (2)) would pass it too...
   Imho it is still a good indication that there are no obvious bugs.
   -/
-theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).fst.contains $ tree.get index := by
+theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (n+1)) (le: α → α → Bool) (index : Fin (n+1)) (h₁ : index ≠ ⟨0, Nat.succ_pos _⟩) : (tree.heapPop le).snd.contains $ tree.get index := by
   unfold heapPop
   split <;> simp
   case isFalse h₃ => omega --contradiction. if n == 0 then index cannot be ≠ 0
@@ -39,7 +39,7 @@ theorem heapPopOnlyRemovesRoot {α : Type u} {n : Nat} (tree : CompleteTree α (
       rw[←h₂] at h₃
       have := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexHeapRemoveLastSameElement tree
       rw[←this] at h₃
-      simp[h₃, heapUpdateRootContainsUpdatedElement]
+      simp[heapPop.Prod.swap,h₃, heapUpdateRootContainsUpdatedElement]
     else
       have h₄ : (Internal.heapRemoveLastWithIndex tree).snd.snd ≠ 0 := by
         have a : n ≠ 0 := Nat.ne_of_gt h₃
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
index dcff870..d8d1de4 100644
--- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
+++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveAt.lean
@@ -5,7 +5,7 @@ import BinaryHeap.CompleteTree.AdditionalProofs.HeapRemoveLast
 
 namespace BinaryHeap.CompleteTree.AdditionalProofs
 
-theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).snd = heap.get index := by
+theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (index : Fin (n+1)) : (heap.heapRemoveAt le index).fst = heap.get index := by
   unfold heapRemoveAt
   if h₁ : index = 0 then
     simp only [h₁, ↓reduceDIte]
@@ -28,7 +28,7 @@ theorem heapRemoveAtReturnsElementAt {α : Type u} {n : Nat} (le : α → α →
         rewrite[←h₄]
         exact Eq.symm $ heapUpdateAtReturnsElementAt le _ _ _
 
-theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).fst.contains (heap.get otherIndex) := by
+theorem heapRemoveAtOnlyRemovesAt {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (removeIndex : Fin (n+1)) (otherIndex : Fin (n+1)) (h₁ : removeIndex ≠ otherIndex) : (heap.heapRemoveAt le removeIndex).snd.contains (heap.get otherIndex) := by
   unfold heapRemoveAt
   if h₂ : removeIndex = 0 then
     subst removeIndex
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean
index aa2eb2c..038a32c 100644
--- a/BinaryHeap/CompleteTree/HeapOperations.lean
+++ b/BinaryHeap/CompleteTree/HeapOperations.lean
@@ -271,18 +271,19 @@ def heapUpdateAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin
 ----------------------------------------------------------------------------------------------
 -- heapPop
 
-def heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : CompleteTree α n × α :=
+def heapPop {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) : α × CompleteTree α n :=
   let l := Internal.heapRemoveLast heap
   if p : n > 0 then
-    heapUpdateRoot p le l.snd l.fst
+    Prod.swap $ heapUpdateRoot p le l.snd l.fst
   else
-    l
+    Prod.swap l
+where Prod.swap := λ(a,b)↦(b,a)
 
 ----------------------------------------------------------------------------------------------
 -- heapRemoveAt
 
 /--Removes the element at a given index. Use `indexOf` to find the respective index.-/
-def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : CompleteTree α n × α :=
+def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) : α × CompleteTree α n :=
   --Since we cannot even temporarily break the completeness property, we go with the
   --version from Wikipedia: We first remove the last element, and then update values in the tree
   --indices are depth first, but "last" means last element of the complete tree.
@@ -292,12 +293,13 @@ def heapRemoveAt {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin
   else
     let (remaining_tree, removed_element, removed_index) := Internal.heapRemoveLastWithIndex heap
     if index = removed_index then
-      (remaining_tree, removed_element)
+      (removed_element, remaining_tree)
     else
       if index_lt_lastIndex : index ≥ removed_index then
         let index := index.pred index_ne_zero
-        heapUpdateAt le index removed_element remaining_tree
+        Prod.swap $ heapUpdateAt le index removed_element remaining_tree
       else
         let h₁ : index < n := by omega
         let index : Fin n := ⟨index, h₁⟩
-        heapUpdateAt le index removed_element remaining_tree
+        Prod.swap $ heapUpdateAt le index removed_element remaining_tree
+where Prod.swap := λ(a,b)↦(b,a)
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean
index df4f9aa..af0593c 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapPop.lean
@@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateRoot
 
 namespace BinaryHeap.CompleteTree
 
-theorem heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapPop le).fst le := by
+theorem heapPopIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapPop le).snd le := by
   have h₂ : HeapPredicate (Internal.heapRemoveLast heap).fst le := CompleteTree.heapRemoveLastIsHeap h₁ wellDefinedLe.left wellDefinedLe.right
-  unfold heapPop
+  unfold heapPop heapPop.Prod.swap
   cases n <;> simp[h₂, heapUpdateRootIsHeap, wellDefinedLe]
diff --git a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean
index 3d7975c..6e0c9e7 100644
--- a/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean
+++ b/BinaryHeap/CompleteTree/HeapProofs/HeapRemoveAt.lean
@@ -3,7 +3,7 @@ import BinaryHeap.CompleteTree.HeapProofs.HeapUpdateAt
 
 namespace BinaryHeap.CompleteTree
 
-theorem heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveAt le index).fst le := by
+theorem heapRemoveAtIsHeap {α : Type u} {n : Nat} (le : α → α → Bool) (index : Fin (n+1)) (heap : CompleteTree α (n+1)) (h₁ : HeapPredicate heap le) (wellDefinedLe : transitive_le le ∧ total_le le) : HeapPredicate (heap.heapRemoveAt le index).snd le := by
   have h₂ : HeapPredicate (Internal.heapRemoveLastWithIndex heap).fst le := CompleteTree.heapRemoveLastWithIndexIsHeap h₁ wellDefinedLe.left wellDefinedLe.right
   unfold heapRemoveAt
   split
diff --git a/BinaryHeap/Relations.lean b/BinaryHeap/Relations.lean
new file mode 100644
index 0000000..ebf45c6
--- /dev/null
+++ b/BinaryHeap/Relations.lean
@@ -0,0 +1,19 @@
+/-
+  This file contains proofs for relations that might be helpful for creating heaps.
+ -/
+import BinaryHeap.HeapPredicate
+
+namespace BinaryHeap
+
+/--Helper for the common case of using natural numbers for sorting.-/
+theorem nat_ble_to_heap_le_total : total_le Nat.ble :=
+  λa b ↦ Nat.ble_eq.substr $ Nat.ble_eq.substr (Nat.le_total a b)
+
+/--Helper for the common case of using natural numbers for sorting.-/
+theorem nat_ble_to_heap_transitive_le : transitive_le Nat.ble :=
+  λ a b c ↦
+    Nat.le_trans (n := a) (m := b) (k := c)
+    |> Nat.ble_eq.substr
+    |> Nat.ble_eq.substr
+    |> Nat.ble_eq.substr
+    |> and_imp.mpr