lean_workbook_plus_4881
ProvedShow that for real
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4881 (a b c : ℝ) : ((a + b) ^ 2 - c ^ 2) * (c ^ 2 - (a - b) ^ 2) ≤ 4 * a ^ 2 * b ^ 2 := by sorry
Source
Show that for real
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_4881 (a b c : ℝ) : ((a + b) ^ 2 - c ^ 2) * (c ^ 2 - (a - b) ^ 2) ≤ 4 * a ^ 2 * b ^ 2 := by sorry