En ℝ, si x ≤ y, entonces y ≰ x ↔ x ≠ y
Demostrar con Lean4 que si \(x\) e \(y\) son números reales tales que \(x ≤ y\), entonces \(y ≰ x ↔ x ≠ y\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x y : ℝ} example (h : x ≤ y) : ¬y ≤ x ↔ x ≠ y := by sorry |