suffices x.stop = x.start + x.size by
  rewrite [this]; exact Nat.add_lt_add_left i.2 x.start
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.start + ↑i < x.stop
α : Type u
x : Subarray α
i : Fin (size x)
⊢ x.stop = x.start + size x