cases Nat.lt_or_eq_of_le hi' with
| inl hlt =>
  have hi' : x.stop ≤ i :=
    Nat.sub_add_cancel (trans x.start.zero_le hrng :) ▸ hlt
  rewrite [get_as_popMax_of_ge_stop lt x i hi']
  exact h.bound_above i k' ⟨hi',hi.2⟩ hk'
| inr heq =>
  cases heq
  rewrite [get_as_popMax_stop_sub_one lt x hrng]
  exact h.is_heap.not_lt_of_descendant k' (.root k')
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
i k : Nat
hi : (BinaryHeap.popMax lt x).stop ≤ i ∧ i < stop
hk : k < Subarray.size (BinaryHeap.popMax lt x)
k' : Nat
hk' : k' < Subarray.size x
left✝ : 0 < k'
hrng : x.start < x.stop
hi' : x.stop - 1 ≤ i
⊢ lt (BinaryHeap.popMax lt x).as[i] x[k'] = false
no goals