lean_workbook_plus_71365
ProvedProve that for positive real numbers and .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_71365 (x y : ℝ) (hx : 0 < x) (hy : 0 < y) : (x + y + 3)⁻¹ - (x + 1)⁻¹ * (y + 1)⁻¹ ≤ 2 / 27 := by sorry
Source