diff options
Diffstat (limited to 'BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean')
| -rw-r--r-- | BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean index 2bdc382..ce9c3e2 100644 --- a/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean +++ b/BinaryHeap/CompleteTree/AdditionalProofs/HeapRemoveLast.lean @@ -76,7 +76,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameTree {α : Type u} {n simp only cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, decide_True, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ + simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ simp only [Nat.add_zero] at h₁ exact absurd h₂.symm h₁ case succ pp => @@ -111,7 +111,7 @@ protected theorem heapRemoveLastWithIndexHeapRemoveLastSameElement {α : Type u} simp only cases p case zero => - simp (config := { ground := true }) only [Nat.zero_add, decide_True, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ + simp (config := { ground := true }) only [Nat.zero_add, decide_true, and_true, Nat.not_lt, Nat.le_zero_eq] at h₂ simp only [Nat.add_zero] at h₁ exact absurd h₂.symm h₁ case succ pp => |