lean_workbook_plus_3062

Proved

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

Setting $p = a + b + c \ge 3$ , then the above inequality becomes \n $2\left( \frac {4}{5} - \frac {3(p^2 - 6)}{5p^2}\right) \ge 3 - \frac {3p}{5}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3062 {p : ℝ} (hp : p ≥ 3) : 2 * (4 / 5 - 3 * (p ^ 2 - 6) / (5 * p ^ 2)) ≥ 3 - 3 * p / 5   :=  by sorry

Source