def choose_succ_right

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

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

170# C(n, k + 1) (k + 1) == C(n, k) (n - k)   (Mathlib Nat.choose_succ_right_eq)
171def choose_succ_right(+n: Nat, +k: Nat) -> {Nat.mul(S.choose(n, 1n+k), 1n+k) == Nat.mul(S.choose(n, k), Nat.sub(n, k)) : Nat}:
172  +c = S.choose(n, k)
173  +d = S.choose(n, 1n+k)
174  # (1 + n) c == c (1 + k) + d (1 + k)
175  +e = Equal.trans(Nat, Nat.mul(1n+n, c), Nat.mul(Nat.add(c, d), 1n+k), Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), succ_mul_choose(n, k), A.mul_add_right(c, d, 1n+k))
176  %Equal.sym(Nat, Nat.mul(c, Nat.sub(n, k)), Nat.sub(Nat.mul(c, 1n+n), Nat.mul(c, 1n+k)), mul_sub_left(c, 1n+n, 1n+k)) : {Nat.mul(d, 1n+k) == _ : Nat}
177  %Equal.sym(Nat, Nat.mul(c, 1n+n), Nat.mul(1n+n, c), A.mul_comm(c, 1n+n)) : {Nat.mul(d, 1n+k) == Nat.sub(_, Nat.mul(c, 1n+k)) : Nat}
178  %Equal.sym(Nat, Nat.mul(1n+n, c), Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), e) : {Nat.mul(d, 1n+k) == Nat.sub(_, Nat.mul(c, 1n+k)) : Nat}
179  Equal.sym(Nat, Nat.sub(Nat.add(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)), Nat.mul(c, 1n+k)), Nat.mul(d, 1n+k), N.add_sub_cancel(Nat.mul(c, 1n+k), Nat.mul(d, 1n+k)))