ForMatUS: Suma de no negativos (en Lean)
En el vídeo se comentan distintas pruebas en Lean de la siguiente propiedad:
Sean a y b números reales. Si 0 ≤ a y 0 ≤ b, entonces 0 ≤ a + b.
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