lean_workbook_plus_53778
ProvedProve that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_53778 : ∀ b c a : ℝ, (b - c + a) * (b + c - a) ≤ b^2 := by sorry
Source
Prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_53778 : ∀ b c a : ℝ, (b - c + a) * (b + c - a) ≤ b^2 := by sorry