feat(Mathlib/Data/Seq/Seq): prove `∀ a ∈ (s : Seq' α), p a` using coinduction

[Komyyy]

---

• [ ] depends on: #13509

This PR consists Continued fractions makes an isomorphism between irrationals and baire space project