Prove2Me

lean_workbook_plus_27984

Proved

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

The remaining n−mn - m teams play (n−m2)\binom{n - m}{2} games among themselves, for a total of (n−m)(n−m−1)(n-m)(n-m-1) points. Again this represents half of the sum of their total points, so their total points is 2(n−m)(n−m−1)=2(n2−2mn+m2−n+m)=2n2−4mn+2m2−2n+2m.2(n-m)(n-m-1) = 2(n^2 - 2mn + m^2 - n + m) = 2n^2 - 4mn + 2m^2 - 2n + 2m.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_27984  (n m : ℕ)
  (h₀ : n > m)
  (h₁ : 0 < m) :
  2 * (n^2 - 2 * n * m + m^2 - n + m) = 2 * n^2 - 4 * n * m + 2 * m^2 - 2 * n + 2 * m   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph