RFC: add Scan iterator combinator

Proposal

This RFC proposes to add IterM.scan IterM.scanM and IterM.scanWithPostcondition (and the corresponding Iter versions).

Over in Batteries, we have been working on adding this combinator to all relevant collections. List.scanl etc. have recently been upstreamed into the stdlib. I already have a pull-request in Batteries (leanprover-community/batteries#1590) adding these combinators for iterators, however after correspondence with @datokrat and @fgdorais it seems as though stdlib is a better place.

Community Feedback

Original Zulip thread (the aforementioned correspondence about upstreaming the iterator versions were regrettably in DMs)

Summary: there is interest in adding scan* combinators to the relevant containers (List, Array, Iterator, Vector). I subsequently made 4 corresponding PRs into batteries. The first two have been merged, and List was subsequently upstreamed. Iterator and Vector are still pending.

Impact

Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.

Start by reviewing the existing iterator APIs in IterM and Iter, then compare the corresponding scan combinators in Batteries PR #1590 and the already-upstreamed List versions. Determine the expected behavior for scan, scanM, and scanWithPostcondition across both iterator types, with completion meaning the relevant combinators are integrated consistently with the standard library.