by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
With x1=21 , x2=17 , x3=16 , x4=14 , again with x12 , x22 , x32 , x42 being the sides of a quadrilateral, gives 4(x2x1+x3x2+x4x3+x1x4)−(x1+x2+x3+x4)(x11+x21+x31+x41)=11910>0
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_48859 (x : ℕ → ℕ) (hx : x 1 = 21 ∧ x 2 = 17 ∧ x 3 = 16 ∧ x 4 = 14) : 4 * (x 1 / x 2 + x 2 / x 3 + x 3 / x 4 + x 4 / x 1) - (x 1 + x 2 + x 3 + x 4) * (1 / x 1 + 1 / x 2 + 1 / x 3 + 1 / x 4) = 10 / 119 := by sorry