Pruebas en Lean de “La relación menor es irreflexiva en los reales”

He añadido a la lista DAO (Demostración Asistida por Ordenador) con Lean el vídeo en el que se comentan 16 pruebas en Lean de la propiedad

La relación menor es irreflexiva en los reales

usando los estilos declarativo, funcional, aplicativo y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada