by_cases start = stop with
| isTrue heq =>
  rw [heq]
  rw [foldl_stop]
  rw [Nat.sub_self]
  rw [Nat.add_zero]
  exact hstop
| isFalse hne =>
  have hstart' : start < stop := Nat.lt_of_le_of_ne hstart hne
  rw [foldl_step push as bs start stop hstart' hstop]
  rw [size_append_aux (start+1) stop hstart' hstop]
  rw [size_push]
  rw [Nat.sub_succ']
  rw [Nat.add_assoc]
  congr
  rw [Nat.add_comm]
  have : 1 ≤ stop - start := by
    rw [Nat.le_sub_iff_add_le hstart]
    rw [Nat.add_comm]
    exact hstart'
  rw [Nat.sub_add_cancel this]
α : Type u_1
as bs : Array α
start stop : Nat
hstart : start ≤ stop
hstop : stop ≤ bs.size
⊢ (foldl push as bs start stop).size = as.size + (stop - start)
no goals