Grace/Cumulus/NumberTheory/BinomialVanishing.g17

Open in Workbench Download source

Imports

Binomial · Nat.Subtraction

Declarations

• choose.vanishes theorem derivation

Source

1-- Binomial coefficients vanish above the row: choose(n, k + 1) = 0 when2-- n ≤ k, with truncated subtraction available for the exponents of the3-- binomial expansion4-- Part of Cumulus, the Grace17 mathematics library.5-- Copyright (c) 2026 Grant Passmore.6-- Released under the Apache License 2.0. See LICENSE in the repository root.7-- Authors: Grant Passmore89module Grace.Cumulus.NumberTheory.BinomialVanishing10import Binomial11import Nat.Subtraction1213theorem choose.vanishes (n k : Nat)14  requires le : n ≤ k15  shows choose(n, succ(k)) = 016proof17  obtain ⟨d, dNat, shape⟩ := le18  have above := choose.above at n19  have form : succ(k) = n + succ(d)20    rw ← shape21    ring22  rw form23  exact above with d, dNat24