ForMatUS: Pruebas en Lean de “Las subsucesiones tienen el mismo límite que la sucesión”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 9 pruebas en Lean de la propiedad

Las subsucesiones de las sucesiones convergentes tienen el mismo límite que la sucesión.

usando los estilos aplicativo, funcional y declarativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada