lean_workbook_plus_52677

Proved

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

Let $x-y=p , x+y-1=q$ we have $x=\frac{p+q+1}{2} , y=\frac{q-p+1}{2}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52677 (x y p q : ℝ) : x - y = p ∧ x + y - 1 = q ↔ x = (p + q + 1) / 2 ∧ y = (q - p + 1) / 2   :=  by sorry

Source