lean_workbook_plus_76112
ProvedLet a and b be real numbers. Prove that,
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76112 (a b: ℝ) : a ^ 2 + b ^ 2 + 1 ≥ a * b + a + b := by sorry
Source
Let a and b be real numbers. Prove that,
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_76112 (a b: ℝ) : a ^ 2 + b ^ 2 + 1 ≥ a * b + a + b := by sorry