lean_workbook_plus_17212

Disproved

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

Equivalent to $(3-q).\left (1-\dfrac{3-q}{\sqrt{q^2-8q+18}+\sqrt{9-2q}}\right )\geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_17212 : ∀ q, (3 - q) * (1 - (3 - q) / (Real.sqrt (q ^ 2 - 8 * q + 18) + Real.sqrt (9 - 2 * q))) ≥ 0   :=  by sorry

Source