diff options
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index cf0774f..d68aedc 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -428,8 +428,7 @@ protected theorem heapRemoveLastWithIndexOnlyRemovesOneElement {α : Type u} {n := by simp only [ne_eq] intro h₁ - have h₂ : n > 0 := by omega - rw[contains_iff_index_exists _ _ h₂] + rw[contains_iff_index_exists _ _] have h₃ := CompleteTree.AdditionalProofs.heapRemoveLastWithIndexRelation heap index simp at h₃ split at h₃ |