have stop_pos : 0 < x.stop :=
  Nat.lt_of_le_of_lt x.start.zero_le hrng
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false
case inl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i j : Nat
hij : i < j
hj : j < stop
hrng : x.start < x.stop
hi : x.stop - 1 ≤ i
stop_pos : 0 < x.stop
⊢ lt (BinaryHeap.popMax lt x).as[j] (BinaryHeap.popMax lt x).as[i] = false