have : x.start < x.stop :=
  trans (x.start.le_add_left n) (Nat.add_lt_of_lt_sub hn)
case succ
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
⊢ lt y✝[j] y✝[i] = false
case succ
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x✝ : Subarray α
stop n✝ : Nat
y : Array α
i j : Nat
hij : i < j
hj : j < stop
x : Subarray α
n : Nat
y✝ : Array α
a✝ : loop.OpSpec lt (BinaryHeap.popMax lt x) n y✝
IH :
  ∀ (h : Algdata.BinaryHeap.heapSort.Intermed lt (BinaryHeap.popMax lt x) stop),
    n ≤ Subarray.size (BinaryHeap.popMax lt x) → (BinaryHeap.popMax lt x).stop - n ≤ i → lt y✝[j] y✝[i] = false
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
hn : n + 1 ≤ Subarray.size x
hi : x.stop - (n + 1) ≤ i
this : x.start < x.stop
⊢ lt y✝[j] y✝[i] = false