lean_workbook_plus_35836

Proved

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

If $x^2+200x+1=y^2$ , then $100^2-1=(x+100)^2-y^2=(x+100+y)(x+100-y)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_35836 y x :  x^2 + 200 * x + 1 = y^2 → 100^2 - 1 = (x + 100)^2 - y^2   :=  by sorry

Source