Challenge 13: Reverse triangle inequality: ||x| - |y|| ≤ |x - y|

José A. Alonso

Lean 4 Challenges/Analysis/Real numbers

Prove the reverse triangle inequality; that is, that for all real numbers \(x\) and \(y\), the following relation holds: \[ ||x| - |y|| ≤ |x - y| \]

To do so, complete the following Lean 4 theory:

import Mathlib.Data.Real.Basic
import Mathlib.Tactic

variable (x y : ℝ)

example : |(|x| - |y|)| ≤ |x - y| :=
by sorry

Calculemus