ForMatUS: Prueba en Lean, mediante reescritura, de la transitividad de la igualdad
En el vídeo se comentan distintas pruebas con Lean de la transitividad de la igualdad de los números reales y cómo se trabaja con ellas en Lean Web. Las primeras son mediante reescritura y las últimas son automáticas.
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