∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} {init : β} {as : Array α} {stop : ℕ} {acc : Array β}
  [inst : Monad m] [LawfulMonad m] {f : α → β → m β} {start : ℕ} {h : start ≤ as.size},
  Array.toList <$> Array.scanrM.loop f init as start stop h acc = do
    let __do_lift ← List.scanrM f init (List.take (start - stop) (List.drop stop as.toList))
    pure (__do_lift ++ acc.toList.reverse)