lean_workbook_plus_71362

Proved

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

Prove that $x^3(1+\sqrt{3-x^2})+x^2\leq 1$ for $x\leq \frac{\sqrt{5}-1}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_71362 : ∀ x : ℝ, x ≤ (Real.sqrt 5 - 1) / 2 ∧ x ≤ 0 → x^3 * (1 + Real.sqrt (3 - x^2)) + x^2 ≤ 1   :=  by sorry

Source