ForMatUS: Pruebas en Lean de P → (Q → R), P, ¬R ⊢ ¬Q

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

P → (Q → R), P, ¬R ⊢ ¬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