simp only [Nat.sub_add_cancel ge_start]
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ k + x.start < x.stop
α : Type u
lt : α → α → Bool
x✝ : Subarray α
n : Nat
y : Array α
i : Nat
x : Subarray α
ge_start : x.start ≤ i
lt_stop : i < x.stop
k : Nat := i - x.start
hki : i = x.start + k
⊢ i < x.stop