Prove2Me

Reordering reciprocal terms in a cyclic expression

Proved
WorkbookSource.problem_40082

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

For real numbers a,b,ca,b,c,

(a2b3−1a)+(b2c3−1b)+(c2a3−1c)=(a2b3−1b)+(b2c3−1c)+(c2a3−1a).\left(\frac{a^2}{b^3}-\frac1a\right)+\left(\frac{b^2}{c^3}-\frac1b\right)+\left(\frac{c^2}{a^3}-\frac1c\right)=\left(\frac{a^2}{b^3}-\frac1b\right)+\left(\frac{b^2}{c^3}-\frac1c\right)+\left(\frac{c^2}{a^3}-\frac1a\right).

At zero denominators the source uses Lean’s total division convention.

Source: InternLM Lean-Workbook, record lean_workbook_40082 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_40082 {a b c : ℝ} : (a^2 / b^3 - 1 / a) + (b^2 / c^3 - 1 / b) + (c^2 / a^3 - 1 / c) = (a^2 / b^3 - 1 / b) + (b^2 / c^3 - 1 / c) + (c^2 / a^3 - 1 / a)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_40082; Apache-2.0

View graph