rewrite [this]
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.stop
α : Type u
x : Subarray α
i : Fin (size x)
this : x.stop = x.start + size x
⊢ x.start + ↑i < x.start + size x