lean_workbook_plus_59761

Proved

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

Given three non-negative numbers $a, b, c$ so that $1\leqq a, b, c\leqq 3$ .\n

\sum\frac{3}{a}+ \frac{45}{a+ b+ c}\geqq\sum\frac{16}{a+ b}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59761 (a b c : ℝ) (ha : 1 ≤ a ∧ a ≤ 3) (hb : 1 ≤ b ∧ b ≤ 3) (hc : 1 ≤ c ∧ c ≤ 3) : 3 / a + 45 / (a + b + c) ≥ 16 / (a + b)   :=  by sorry

Source

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

View graph