Prove2Me

lean_workbook_plus_29688

Proved

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

Let a2+(b−c)2=x\sqrt{a^2+\left(b-c\right)^2}=x and similar for yy and zz . Show that x2+y2−z2≥0x^2+y^2-z^2 \geq 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_29688 (a b c x y z : ℝ) (hx : x = Real.sqrt (a ^ 2 + (b - c) ^ 2)) (hy : y = Real.sqrt (b ^ 2 + (c - a) ^ 2)) (hz : z = Real.sqrt (c ^ 2 + (a - b) ^ 2)) : x ^ 2 + y ^ 2 - z ^ 2 ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph