ForMatUS: La suma de no negativos es expansiva (en Lean)

En el vídeo se prueba en Lean las siguientes propiedades de los números reales:

• Si 0 ≤ a, entonces b ≤ a + b.
• Si 0 ≤ b, entonces a ≤ 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