Prove2Me

The formula for choosing two elements

Proved
WorkbookRestored.plus_3413

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

lean-workbookrestored-importssource-checked

For every natural number xx,

(x2)=x2−x2.\binom x2=\frac{x^2-x}{2}.

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

Preamble
import Mathlib.Data.Nat.Choose.Basic
open Nat
Formal statement
theorem WorkbookRestored.plus_3413 : ∀ x : ℕ, choose x 2 = (x^2 - x) / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_3413; original Prove2Me node 0dbee549-c42f-4a38-a3de-06084b532386; Apache-2.0

View graph