lean_workbook_plus_39654

Proved

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

Let $a,$ $b,$ $c$ be the side-lengths of a triangle. Prove that \n $a^2\left(\frac {b}{c} - 1\right) + b^2\left(\frac {c}{a} - 1\right) + c^2\left(\frac {a}{b} - 1\right) \ge 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39654    (a b c : ℝ)
    (h₁ : 0 < a ∧ 0 < b ∧ 0 < c)
    (h₂ : c < a + b)
    (h₃ : b < a + c)
    (h₄ : a < b + c) :
    0 ≤ a^2 * (b / c - 1) + b^2 * (c / a - 1) + c^2 * (a / b - 1)   :=  by sorry

Source

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

View graph