def choose_one_right

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

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

128# C(n, 1) == n
129def choose_one_right(+n: Nat) -> {S.choose(n, 1n) == n : Nat}:
130  match n:
131    case 0n:
132      {==}
133    case 1n+ +m:
134      %Equal.sym(Nat, S.choose(m, 0n), 1n, choose_zero_right(m)) : {Nat.add(_, S.choose(m, 1n)) == 1n+m : Nat}
135      N.succ_cong(S.choose(m, 1n), m, choose_one_right(m))