ForMatUS: Suma de desigualdades (en Lean)

En el vídeo se comentan distintas pruebas en Lean de la siguiente propiedad:

Sean a, b, c y d números reales. Si a ≤ b y c ≤ d, entonces a + c ≤ b + d.

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