have : 1 ≤ stop - start := by
  rw [Nat.le_sub_iff_add_le hstart]
  rw [Nat.add_comm]
  exact hstart'
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
⊢ stop - start - 1 + 1 = stop - start
case e_a
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
hne : ¬start = stop
hstart' : start < stop
this : 1 ≤ stop - start
⊢ stop - start - 1 + 1 = stop - start