Prove2Me

lean_workbook_plus_60479

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

So it remains to show y+∣x−y+z∣≥∣x−y∣+∣y−z∣ y + |x - y + z|\geq |x - y| + |y - z| for nonnegative x,y,z x,y,z . This is equivalent to the square of the inequality,   ⟺  y2+(x−y+z)2+2y∣x−y+z∣≥(x−y)2+(y−z)2+2∣x−y∣∣y−z∣ \iff y^2 + (x - y + z)^2 + 2y|x - y + z|\geq (x - y)^2 + (y - z)^2 + 2|x - y||y - z|

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_60479 (x y z : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) : y + |x - y + z| ≥ |x - y| + |y - z|   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph