feat: add finite and well-founded streams

[fgdorais]

Add classes for provably finite streams and connect streams with standard library iterators.

[leanprover-community-bot]

Mathlib CI status (docs):

• ✅ Mathlib branch batteries-pr-testing-1331 has successfully built against this PR. (2025-07-18 11:55:38) View Log

[kim-em]

Could you explain how this relates to the core iterators? What is the use case that is not being filled by those?

[fgdorais]

Could you explain how this relates to the core iterators?

The connection with iterators was in a follow-up PR #1372. I've closed that one and merged with this one.

What is the use case that is not being filled by those?

The main purpose is to help people port their stream-based code to iterator-based code.