lean_workbook_plus_52997

Proved

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

Prove that $\frac{xy(2+x+y)}{(1+x)(1+y)} \leqslant \frac{1+x+y}{3}$ given $0<x<1$ , $0<y<1$ , and $x+y>1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52997 (x y : ℝ) (hx : 0 < x ∧ x < 1) (hy : 0 < y ∧ y < 1) (h : x + y > 1) :
  (x * y * (2 + x + y)) / ((1 + x) * (1 + y)) ≤ (1 + x + y) / 3   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph