lean_workbook_plus_35937

Proved

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

Given $x, y, z$ are sides of a triangle, prove: $\frac{xyz}{(-x+y+z) (x-y+z) (x+y-z)} \geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35937 {x y z : ℝ} (hx : 0 < x ∧ 0 < y ∧ 0 < z) (hx1 : y + z > x) (hx2 : z + x > y) (hx3 : x + y > z) : (x * y * z) / ((-x + y + z) * (x - y + z) * (x + y - z)) ≥ 1   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph