Pruebas en Lean de “Toda sucesión convergente es una sucesión de Cauchy”

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

Toda sucesión convergente es una sucesión de Cauchy

usando los estilos aplicativo y declarativo.

A continuación, se muestra el vídeo

y el código de la teoría utilizada