ForMatUS: Prueba en Lean mediante encadenamiento de ecuaciones

En el vídeo se comentan distintas pruebas con Lean de una igualdad con productos de números reales. La primera es por reescritura usando las propiedades asociativa y conmutativa, La segunda es con encadenamiento de ecuaciones. Las restantes 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