apply foldrM_step
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ foldr f b as (start + 1) stop = foldr f (f as[start] b) as start stop
case hstop
α : Type u_1
β : Type u_2
f : α → β → β
b : β
as : Array α
start stop : Nat
hstop : stop ≤ start
hstart : start < as.size
⊢ stop ≤ start