simp only [Array.getElem_swap, Subarray.castIndex]
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (Array.swap x.as (Subarray.castIndex x { val := 0, isLt := (_ : 0 < x.stop - x.start) })
        (Subarray.castIndex x
          { val := Subarray.size x - 1,
            isLt := (_ : Nat.pred (Nat.sub (Subarray.size x) 0) < Nat.sub (Subarray.size x) 0) }))[x.stop - 1] =
    x[0]
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ (if x.start + (Subarray.size x - 1) = x.stop - 1 then x.as[x.start + 0]
    else if x.start + 0 = x.stop - 1 then x.as[x.start + (Subarray.size x - 1)] else x.as[x.stop - 1]) =
    x[0]