induction h' with
| zero => exact h.sorted i j hi hij hj
| @succ x n _ _ IH =>
  have : x.start < x.stop :=
    trans (x.start.le_add_left n) (Nat.add_lt_of_lt_sub hn)
  refine @IH h.popMax ?_ ?_
  . exact size_popMax lt x ▸ Nat.le_sub_of_add_le hn
  . rewrite [stop_popMax lt x this, Nat.sub_sub, Nat.add_comm]
    exact hi
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop n : Nat
y : Array α
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
h' : loop.OpSpec lt x n y
hn : n ≤ Subarray.size x
i j : Nat
hi : x.stop - n ≤ i
hij : i < j
hj : j < stop
⊢ lt y[j] y[i] = false
no goals