ForMatUS: Pruebas en Lean de ¬Q → ¬P ⊢ P → ¬¬Q

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 15 pruebas en Lean de

¬Q → ¬P ⊢ P → ¬¬Q

usando los estilos declarativos, aplicativos, funcional y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada