lean_workbook_plus_46671

Proved

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

Solve for x and y in the system of equations: ${\begin{cases}x-y=p\\x+y=q\end{cases}}$ where $pq=240$ and $p\leqslant q$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_46671 (p q x y : ℝ) (h₁ : x - y = p) (h₂ : x + y = q) (h₃ : p * q = 240) (h₄ : p ≤ q) : x = (q + p) / 2 ∧ y = (q - p) / 2   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph