Prove2Me

lean_workbook_plus_70353

Proved

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

Prove that for n=3n=3, if 0<a≤b≤c0 < a \leq b \leq c, then ab+bc+ca≥ba+cb+ac\frac{a}{b} + \frac{b}{c} + \frac{c}{a} \geq \frac{b}{a} + \frac{c}{b} + \frac{a}{c}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70353 (a b c : ℝ) (h₁ : 0 < a ∧ 0 < b ∧ 0 < c) (h₂ : a ≤ b ∧ b ≤ c) : a / b + b / c + c / a ≥ b / a + c / b + a / c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph