rw [Nat.sub_succ']
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - (start + 1)) = as.size + (stop - start)
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ as.size + 1 + (stop - start - 1) = as.size + (stop - start)