lean_workbook_plus_39497

Proved

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

Prove the inequality $(\sqrt{3}x - 1)^2(2x + \sqrt{3}) \geq 0$ for $x \in (0, 1)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_39497 (x : ℝ) (hx : 0 < x ∧ x < 1) :
  0 ≤ ((Real.sqrt 3) * x - 1)^2 * (2 * x + Real.sqrt 3)   :=  by sorry

Source