lean_workbook_plus_18289
ProvedIs this true: ?
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18289 (a b : ℝ) : a^2 * b^2 + a^2 + b^2 + 2 * (a + b) + 1 ≥ 2 * (a^2 * b + a * b^2) := by sorry
Source
Is this true: ?
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_18289 (a b : ℝ) : a^2 * b^2 + a^2 + b^2 + 2 * (a + b) + 1 ≥ 2 * (a^2 * b + a * b^2) := by sorry