lean_workbook_plus_51032

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

For positive numbers a, b, c, d satisfy $a> c$ , $b> d$ . Prove that: $\sqrt{a+b} - \sqrt{c} - \sqrt{d} > \sqrt{c+d}- \sqrt{a} - \sqrt{b}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_51032 (a b c d : ℝ) (h₁ : a > c) (h₂ : b > d) (h₃ : 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d) : Real.sqrt (a + b) - Real.sqrt c - Real.sqrt d > Real.sqrt (c + d) - Real.sqrt a - Real.sqrt b   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph