En ℝ, si x ≠ 0 entonces x < 0 ó x > 0
Demostrar con Lean4 que en ℝ, si \(x ≠ 0\) entonces \(x < 0\) ó \(x > 0\).
Para ello, completar la siguiente teoría de Lean4:
|
1 2 3 4 5 6 7 |
import Mathlib.Data.Real.Basic variable {x : ℝ} example (h : x ≠ 0) : x < 0 ∨ x > 0 := by sorry |