lean_workbook_plus_32057

Disproved

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

It est, it remains to prove that $\frac{t+2}{t+1}\geq3-\frac{3t}{2}$ , which is $(t-1)(3t+2)\geq0$ , \n which is obvious.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32057 : ∀ t : ℝ, t > 0 → ((t + 2) / (t + 1) ≥ 3 - (3 * t) / 2)   :=  by sorry

Source