ForMatUS: Prueba en Lean con hipótesis y uso de lemas
En el vídeo se comentan distintas pruebas con Lean de una propiedad de la aritmética de los números reales con hipótesis. La primera es por reescritura y la segunda es con encadenamiento de ecuaciones. Las restantes son automáticas.
El enlace a la sesión es
Los enlaces correspondientes son: a la sesión en Lean Web, al código y al libro “DAO con Lean”.
A continuación, se muestra el vídeo