lean_workbook_plus_140
ProvedProve for all real x,y
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_140 (x y: ℝ): x ^ 2 + x + y ^ 2 + y + 1 ≥ x * y := by sorry
Source
Prove for all real x,y
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_140 (x y: ℝ): x ^ 2 + x + y ^ 2 + y + 1 ≥ x * y := by sorry