lean_workbook_plus_2420

Proved

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

If $x,y$ are pozitive real numbers such that $x+y+xy=3$ .Prove that $x+y\geq 2$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_2420 (x y : ℝ) (hxy : 0 < x ∧ 0 < y) (h : x + y + x * y = 3) : x + y ≥ 2   :=  by sorry

Source