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