lean_workbook_plus_10489
ProvedPreamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10489 (a b : ℝ) : 5 * (a ^ 4 + b ^ 4) + 6 * a ^ 2 * b ^ 2 ≥ 8 * (a * b ^ 3 + b * a ^ 3) := by sorry
Source
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_10489 (a b : ℝ) : 5 * (a ^ 4 + b ^ 4) + 6 * a ^ 2 * b ^ 2 ≥ 8 * (a * b ^ 3 + b * a ^ 3) := by sorry