lean_workbook_plus_25128
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_25128 (b c : ℝ) : (b + c) ^ 4 ≤ 16 * (b ^ 4 - b ^ 2 * c ^ 2 + c ^ 4) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_25128 (b c : ℝ) : (b + c) ^ 4 ≤ 16 * (b ^ 4 - b ^ 2 * c ^ 2 + c ^ 4) := by sorry