lean_workbook_plus_59134

Proved

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

Let $a,b,c\in R$ , $|a|\geq |b+c|$ , $|b|\geq |c+a|$ , $|c|\geq |a+b|$ . Prove: $a+b+c=0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59134 (a b c : ℝ) (hab : |a| ≥ |b + c|) (hbc : |b| ≥ |c + a|) (hca : |c| ≥ |a + b|) : a + b + c = 0   :=  by sorry

Source