Negación del universal en Lean: Caracterización de funciones no pares

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

¬par f ↔ ∃ x, f (-x) ≠ f x

usando los estilos declarativo, aplicativo y automático.

A continuación, se muestra el vídeo

y el código de la teoría utilizada