{x ≤ y, y ≰ x} ⊢ x ≤ y ∧ x ≠ y
Demostrar con Lean4 que
\[\{x ≤ y, y ≰ x\} ⊢ x ≤ y ∧ x ≠ y\]
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 8 9 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h1 : x ≤ y) (h2 : ¬y ≤ x) : x ≤ y ∧ x ≠ y := by sorry |