ForMatUS: Pruebas en Lean de que las partes simétricas son simétricas

He añadido a la lista Lógica con Lean el vídeo en el que se comentan 6 pruebas en Lean de la siguiente propiedad: “Si R es una relación, entonces su parte simétrica (es decir, la relación S definida por S x y := R x y ∧ R y x) es simétrica”, 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