def desc_zero

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/natfuel.bend:417

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-math@1.0.0.0/spec/math/natural.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA

417def desc_zero(+n: Nat, +k: Nat, +h: {Nat.is_lt(n, k) == True{} : Bool}) -> {S.desc(n, k) == 0n : Nat}:
418  Equal.trans(Nat, S.desc(n, k), Nat.mul(S.choose(n, k), S.factorial(k)), 0n, Equal.sym(Nat, Nat.mul(S.choose(n, k), S.factorial(k)), S.desc(n, k), FA.choose_mul_factorial(n, k)), Equal.trans(Nat, Nat.mul(S.choose(n, k), S.factorial(k)), Nat.mul(0n, S.factorial(k)), 0n, Equal.cong(Nat, Nat, t => Nat.mul(t, S.factorial(k)), S.choose(n, k), 0n, FA.choose_eq_zero(n, k, h)), Equal.trans(Nat, Nat.mul(0n, S.factorial(k)), Nat.mul(S.factorial(k), 0n), 0n, NA.mul_comm(0n, S.factorial(k)), NA.mul_zero(S.factorial(k)))))