lean_workbook_plus_58551

Proved

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

Prove the lemma: For positive $a, b, c, d$ , if $\frac{a}{b}>\frac{c}{d}$ , then $\frac{a}{b}>\frac{a+c}{b+d}>\frac{c}{d}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58551 (a b c d : ℝ) (h1 : 0 < a ∧ 0 < b ∧ 0 < c ∧ 0 < d) (h2 : a / b > c / d) : a / b > (a + c) / (b + d) ∧ (a + c) / (b + d) > c / d   :=  by sorry

Source

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

View graph