Prove2Me

Counting ordered pairs of distinct elements

Proved
WorkbookRestored.plus_3121

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrestored-importssource-checked

For every natural number nn,

n(n−1)=2(n2).n(n-1)=2\binom n2.

This restores the missing imports or namespaces of the original node, retaining its formal proposition. Source: Lean-Workbook row lean_workbook_plus_3121 (Apache-2.0).

Preamble
import Mathlib.Data.Nat.Choose.Basic
open Nat
Formal statement
theorem WorkbookRestored.plus_3121 (n : ℕ) : n * (n - 1) = 2 * choose n 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_3121; original Prove2Me node d8bf9e24-d293-4827-80c9-1d69e9d45a65; Apache-2.0

View graph