delta popMax
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk, 0 < k ∧ (popMax lt x)[i] = x[k]
α : Type u
lt : α → α → Bool
x : Subarray α
i : Nat
hi : i < Subarray.size x - 1
⊢ ∃ k hk,
    0 < k ∧
      (if h : x.start < x.stop then
            let_fun this := (_ : 0 < x.stop - x.start);
            let x :=
              Subarray.swap x { val := 0, isLt := this }
                { val := Subarray.size x - 1,
                  isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) };
            heapifyDown lt (Subarray.shrinkOne' x h) 0
          else x)[i] =
        x[k]