lean_workbook_plus_54451

Proved

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

Case 2: $t_1+t_2\geq t_1t_2+1$ then $(t_{2}+1)^{2}(t_{1}+1)^{2}=(t_1+t_2+t_1t_2+1)^2\geq 4(t_1t_2+1)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54451 (t1 t2 : ℕ) (h : t1 + t2 ≥ t1 * t2 + 1) :
  (t2 + 1)^2 * (t1 + 1)^2 ≥ 4 * (t1 * t2 + 1)^2   :=  by sorry

Source