lean_workbook_plus_59684

Proved

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

Given that $0\le a\le b\le c$ , prove that

(a+b+2)(b+c+4)(c+a+6)\ge 8(a+1)(b+2)(c+3)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_59684 (a b c : ℝ) (ha : 0 ≤ a) (hb : a ≤ b) (hc : b ≤ c) : (a + b + 2) * (b + c + 4) * (c + a + 6) ≥ 8 * (a + 1) * (b + 2) * (c + 3)   :=  by sorry

Source

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

View graph