En ℝ, x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x
Demostrar con Lean4 que. en \(ℝ\), \(x ≤ y ∧ x ≠ y → x ≤ y ∧ y ≰ x\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 |
import Mathlib.Data.Real.Basic variable (x y : ℝ) example : x ≤ y ∧ x ≠ y → x ≤ y ∧ ¬ y ≤ x := by sorry |