lean_workbook_plus_69113
Proved[Simpler solution]
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_69113 (x y z : ℝ) : x + y + z ≤ 2 + x * y * z ↔ x * (1 - y * z) + y + z ≤ 2 := by sorry
Source
[Simpler solution]
import Mathlib.Analysis.Complex.Basic
theorem lean_workbook_plus_69113 (x y z : ℝ) : x + y + z ≤ 2 + x * y * z ↔ x * (1 - y * z) + y + z ≤ 2 := by sorry