lean_workbook_plus_44862
ProvedFor real a,b prove that
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_44862 (a b : ℝ) : a^6 + 3*a^4*b^2 + 8*b^6 >= 2*a^3*b^3 + 2*a^2*b^4 + 8*a*b^5 := by sorry
Source
For real a,b prove that
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_44862 (a b : ℝ) : a^6 + 3*a^4*b^2 + 8*b^6 >= 2*a^3*b^3 + 2*a^2*b^4 + 8*a*b^5 := by sorry