rewrite [get_as_popMax_stop_sub_one lt x hrng]
case inl.inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
j : Nat
hj : j < stop
hrng : x.start < x.stop
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hij : x.stop - 1 < j
hi : x.stop - 1 ≤ x.stop - 1
⊢ lt x.as[j] (BinaryHeap.popMax lt x).as[x.stop - 1] = false
case inl.inr.refl
α : Type u
lt : α → α → Bool
inst✝ : LawfulLTBRel lt
x : Subarray α
stop : Nat
h : Algdata.BinaryHeap.heapSort.Intermed lt x stop
j : Nat
hj : j < stop
hrng : x.start < x.stop
stop_pos : 0 < x.stop
this : x.stop - 1 + 1 = x.stop
hj' : x.stop ≤ j
hij : x.stop - 1 < j
hi : x.stop - 1 ≤ x.stop - 1
⊢ lt x.as[j] x[0] = false