def cstep

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/combnat.bend:46

import Base
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/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/natural/fact.bend as FA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

46# 1 + 2 i <= n gives C(n, i) <= C(n, 1 + i)
47def cstep(+n: Nat, +i: Nat, +h: {Nat.is_le(1n+Nat.double(i), n) == True{} : Bool}) -> {Nat.is_le(S.choose(n, i), S.choose(n, 1n+i)) == True{} : Bool}:
48  +c = S.choose(n, i)
49  +c1 = S.choose(n, 1n+i)
50  +hs = L.subst(Nat, z => {Nat.is_le(z, Nat.sub(n, i)) == True{} : Bool}, Nat.sub(1n+Nat.double(i), i), 1n+i, sub_half(i), NF.sub_mono_l(1n+Nat.double(i), n, i, h))
51  +h1 = NF.mul_le_r(c, 1n+i, Nat.sub(n, i), hs)
52  +h2 = L.subst(Nat, z => {Nat.is_le(Nat.mul(c, 1n+i), z) == True{} : Bool}, Nat.mul(c, Nat.sub(n, i)), Nat.mul(c1, 1n+i), Equal.sym(Nat, Nat.mul(c1, 1n+i), Nat.mul(c, Nat.sub(n, i)), FA.choose_succ_right(n, i)), h1)
53  le_cancel(c, c1, i, h2)