lean_workbook_plus_75716

Proved

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

Given $(b+c)^{2}+(b-c)^{2}=2\left(b^{2}+c^{2}\right)$ , prove that $|b-c|=\sqrt{2\left(b^{2}+c^{2}\right)-(b+c)^{2}}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_75716 (b c : ℝ) : |b - c| = Real.sqrt (2 * (b^2 + c^2) - (b + c)^2)   :=  by sorry

Source