feat: add Scan iterator combinator

[cmlsharp]

This PR adds IterM.scanWithPostcondition IterM.scanM, IterM.scan Iter.scanWithPostcondition, IterM.scanM, Iter.scan as well as corresponding theorems that prove their equivalence to their List counterparts. It additionally upstreams Bool.lt_wf and Bool.gt_wf from Batteries.Data.Bool.

This PR is based on leanprover-community/batteries#1590. However after private correspondence with @datokrat and @fgdorais, I was asked to create an PR adding it into the stdlib.

The Bool.lt_wf and Bool.gt_wf additions can be extracted out into a separate PR if that is desirable. Or if there is some reason not to upstream them at all, it would not be too difficult to rewrite the proof not to require it.

Closes: #12741

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-02-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-03-01 02:42:14)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-02-28 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-01 02:42:16)