lean_workbook_plus_16358
Proveda, b are positive reals such that $a+b = 1$ . Prove that \n$\frac{1}{3}\leq \frac{a^{2}}{a+1}+\frac{b^{2}}{b+1}< \frac{1}{2}$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16358 (a b : ℝ) (ha : a > 0) (hb : b > 0) (hab : a + b = 1) : 1 / 3 ≤ a ^ 2 / (a + 1) + b ^ 2 / (b + 1) ∧ a ^ 2 / (a + 1) + b ^ 2 / (b + 1) < 1 / 2 := by sorry
Source