diff options
| -rw-r--r-- | BinaryHeap/CompleteTree/HeapOperations.lean | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/BinaryHeap/CompleteTree/HeapOperations.lean b/BinaryHeap/CompleteTree/HeapOperations.lean index a8ac1be..5ddccd5 100644 --- a/BinaryHeap/CompleteTree/HeapOperations.lean +++ b/BinaryHeap/CompleteTree/HeapOperations.lean @@ -65,7 +65,14 @@ def heapPush (le : α → α → Bool) (elem : α) (heap : CompleteTree α o) : match subtree_complete with | .inl h₂ => absurd h₂ h₁ | .inr h₂ => power_of_two_mul_two_lt h₂ max_height_difference h₁ - let result := branch a (left.heapPush le elem) right (Nat.le_succ_of_le p) still_in_range (Or.inr right_is_power_of_two) + let result := + branch + a + (left.heapPush le elem) + right + (Nat.le_succ_of_le p) + still_in_range + (Or.inr right_is_power_of_two) have letMeSpellItOutForYou : n + 1 + m + 1 = n + m + 1 + 1 := (Nat.add_assoc n 1 m).subst (motive := λx↦n+1+m+1=x+1) rfl |> (Nat.add_comm 1 m).subst (motive := λx↦n+1+m+1=n+(x)+1) |