lean_workbook_plus_65608

Proved

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

Observe that $\frac{(a+b)(1-ab)}{(1+a^2)(1+b^2)} \le \frac{1}{2} \iff (1+a^2)(1+b^2) - 2(a+b)(1-ab) = (ab+a+b-1)^2 \ge 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65608 (a b : ℝ) : (a + b) * (1 - a * b) / ((1 + a ^ 2) * (1 + b ^ 2)) ≤ 1 / 2 ↔ (a * b + a + b - 1) ^ 2 ≥ 0   :=  by sorry

Source