En ℝ, si x < |y|, entonces x < y ó x < -y
Demostrar con Lean4 que en \(ℝ\), si \(x < |y|\), entonces \(x < y\) ó \(x < -y\).
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 := by sorry |