lean_workbook_plus_58457

Proved

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

Since the thesis, we write the inequality in equivalent form: \n\n $\sum_{cyc}{(a-b)^{2}\over ab}\cdot{(a-c)^{2}\over ac}\geq 0.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58457 (a b c : ℝ) : (a - b) ^ 2 / a / b * (b - c) ^ 2 / b / c * (c - a) ^ 2 / c / a ≥ 0   :=  by sorry

Source