Si ≤ es un preorden, entonces < es irreflexiva
Demostrar con Lean4 que si \(≤\) es un preorden, entonces \(<\) es irreflexiva.
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 |
import Mathlib.Tactic variable {α : Type _} [Preorder α] variable (a : α) example : ¬a < a := by sorry |