lean_workbook_plus_62276

Proved

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

If ${a\geq b\geq 0,\ c\geq d\geq 0,\ a\leq c}$ and ${ab\leq cd}$ , then prove that ${a+b\leq c+d}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_62276 (a b c d : ℝ) (h1 : a ≥ b ∧ b ≥ 0) (h2 : c ≥ d ∧ d ≥ 0) (h3 : a ≤ c) (h4 : a * b ≤ c * d) : a + b ≤ c + d   :=  by sorry

Source

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

View graph