∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (f : α → β → m β) (init : β) (as : Array α)
  (start stop : ℕ), Array.scanrM f init as start stop = Array.scanrM.loop f init as (min start as.size) stop ⋯ #[]