cases Nat.lt_or_eq_of_le hi with
| inl hlti =>
  have : x.stop ≤ i :=
    ‹x.stop-1+1=x.stop› ▸ (hlti : x.stop-1+1 ≤ i)
  rewrite [get_as_popMax_of_ge_stop lt x i this]
  exact h.sorted i j this hij hj
| inr heqi =>
  cases heqi
  rewrite [get_as_popMax_stop_sub_one lt x hrng]
  exact h.bound_above j 0 ⟨hj',hj⟩ _
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
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[i] = false
no goals