rw [Nat.sub_self]
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + (stop - stop)

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ as.size = as.size + 0

case hstop
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
heq : start = stop
⊢ stop ≤ bs.size