def choose_eq_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/fact.bend:194

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/math/natural.bend as S

194# n < k gives C(n, k) == 0   (Mathlib Nat.choose_eq_zero_of_lt)
195def choose_eq_zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> {S.choose(n, k) == 0n : Nat}:
196  match n k:
197    case n0 0n:
198      Empty.absurd({S.choose(n0, 0n) == 0n : Nat}, N.lt_zero_absurd(n0, h))
199    case 0n 1n+j:
200      {==}
201    case 1n+ +m 1n+ +j:
202      %Equal.sym(Nat, S.choose(m, j), 0n, choose_eq_zero(m, j, h)) : {Nat.add(_, S.choose(m, 1n+j)) == 0n : Nat}
203      choose_eq_zero(m, 1n+j, N.lt_trans(m, j, 1n+j, h, N.lt_succ(j)))