rw [Nat.sub_succ, heq, Nat.pred_succ]
case e_a.h
β : Type u_3
α : Type u_1
m : Type u_3 → Type u_2
inst✝ : Monad m
f : β → α → m β
b✝ : β
as : Array α
start stop : Nat
hstart : start < stop
hstop : stop ≤ as.size
i✝ i'✝ : Nat
heq : stop - start = i'✝.succ
b : β
⊢ foldlM.loop f as stop ⋯ i'✝ (start + 1) b = foldlM.loop f as stop ⋯ (stop - (start + 1)) (start + 1) b
no goals