ForMatUS: Pruebas en Lean de que las partes estrictas de los órdenes parciales son transitivas

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 2 pruebas en Lean de que las partes estrictas de los órdenes parciales son transitivas usando los estilos aplicativos y declarativos.

A continuación, se muestra el vídeo

y el código de la teoría utilizada