rfl
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.as[x.start + 0] = x[0]

case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1
case hc
α : Type u
lt : α → α → Bool
x : Subarray α
hs : x.start < x.stop
⊢ x.start + (Subarray.size x - 1) = x.stop - 1