Adding scan combinators to batteries

Stream: PR reviews

[cmlsharp]

https://github.com/leanprover-community/batteries/pull/1581

This implements scanlM scanlR for List and scanl/scanr/scanlM/scanrM for Array. Along with a (yet incomplete) set of theorems about them. Tail recursive implementations are provided for the list functions as well as efficient usize-index versions for the Array functions. The eventual goal is to do something similar for Vector and Iterator.

I'm pretty new to lean. This is my first PR. I would appreciate any guidance or comments anyone has. In particular a couple of the proofs relating to Array.scanrMcould hopefully be simplified.