ForMatUS: Monotonía de la multiplicación por no positivo (en Lean)

En el vídeo se comentan 5 demostraciones en Lean de la siguiente propiedad:

Sean a, b y c números reales. Si c ≤ 0 y a ≤ b, entonces bc ≤ ac.

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