rewrite [get_as_heapifyDown_of_ge_stop lt _ 0 (x.stop-1)]
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (heapifyDown lt
          (Subarray.shrinkOne'
            (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
              { val := Subarray.size x - 1,
                isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
            (_ : x.start < x.stop))
          0).as[x.stop - 1] =
    x[0]
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Subarray.shrinkOne'
          (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
            { val := Subarray.size x - 1,
              isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
          (_ : x.start < x.stop)).as[x.stop - 1] =
    x[0]

α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.stop - 1 ≥
    (Subarray.shrinkOne'
        (Subarray.swap x { val := 0, isLt := (_ : 0 < x.stop - x.start) }
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) })
        (_ : x.start < x.stop)).stop