lean_workbook_plus_12047
Proved(x^{2}+1)(y^{2}+1) \geq (xy+1)^{2} x ,y \geq 0$
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_12047 (x y : ℝ) (hx : x ≥ 0) (hy : y ≥ 0) : (x^2 + 1) * (y^2 + 1) ≥ (x * y + 1)^2 := by sorry
Source