lean_workbook_plus_54844

Proved

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

Let $a = xy$ , $b = x-y$ . Then, $a + b + 1 = ab - 2 \Longleftrightarrow (a-1)(b-1) = 4$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54844 (a b: ℤ) : a + b + 1 = a * b - 2 ↔ (a-1) * (b-1) = 4   :=  by sorry

Source