lean_workbook_plus_29698

Proved

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

Given the inequality $x^2+y^2+1 \geq xy+x+y$ for real numbers x and y, find the solution using the substitution $p=x-1$ and $q=1-y$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29698 (x y p q : ℝ) (hp : p = x - 1) (hq : q = 1 - y) : p^2 + q^2 + 1 ≥ p * q + p + q   :=  by sorry

Source