lean_workbook_plus_67412

Proved

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

Show that for all real numbers $x$ and $y$ with $x > -1$ and $y > -1$ and $x + y = 1$ the inequality \n\n

\frac{x}{y + 1} +\frac{y}{x + 1} \ge \frac23

\nholds. When does equality apply?\n\n(Walther Janous)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67412 (x y : ℝ) (hx : x > -1) (hy : y > -1) (hxy : x + y = 1) : (x / (y + 1) + y / (x + 1)) ≥ 2 / 3   :=  by sorry

Source