-- Binomial coefficients vanish above the row: choose(n, k + 1) = 0 when
-- n ≤ k, with truncated subtraction available for the exponents of the
-- binomial expansion
-- Part of Cumulus, the Grace17 mathematics library.
-- Copyright (c) 2026 Grant Passmore.
-- Released under the Apache License 2.0. See LICENSE in the repository root.
-- Authors: Grant Passmore

module Grace.Cumulus.NumberTheory.BinomialVanishing
import Binomial
import Nat.Subtraction

theorem choose.vanishes (n k : Nat)
  requires le : n ≤ k
  shows choose(n, succ(k)) = 0
proof
  obtain ⟨d, dNat, shape⟩ := le
  have above := choose.above at n
  have form : succ(k) = n + succ(d)
    rw ← shape
    ring
  rw form
  exact above with d, dNat