simp only [sum]
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ let_fun this := ⋯;
  ns.sum start stop = ns[start] + ns.sum (start + 1) stop
ns : Array Nat
start stop : Nat
hstart : start < stop
hstop : stop ≤ ns.size
this : start < ns.size
⊢ foldl (fun x x_1 => x + x_1) 0 ns start stop = ns[start] + foldl (fun x x_1 => x + x_1) 0 ns (start + 1) stop