def cmono_d

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

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/nat.bend as N
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/lib/lemmas/proofs/nat_algebra.bend as NA

55# 2 (i + d) <= n gives C(n, i) <= C(n, i + d)
56def cmono_d(+n: Nat, +i: Nat, +d: Nat, +h: {Nat.is_le(Nat.double(Nat.add(i, d)), n) == True{} : Bool}) -> {Nat.is_le(S.choose(n, i), S.choose(n, Nat.add(i, d))) == True{} : Bool}:
57  match d:
58    case 0n:
59      L.subst(Nat, z => {Nat.is_le(S.choose(n, i), S.choose(n, z)) == True{} : Bool}, i, Nat.add(i, 0n), Equal.sym(Nat, Nat.add(i, 0n), i, N.add_zero(i)), N.le_refl(S.choose(n, i)))
60    case 1n+ +dp:
61      +s = Nat.add(i, dp)
62      +es = NA.add_succ(i, dp)
63      +h1 = L.subst(Nat, z => {Nat.is_le(Nat.double(z), n) == True{} : Bool}, Nat.add(i, 1n+dp), 1n+s, es, h)
64      +h2 = N.le_trans(1n+Nat.double(s), Nat.double(1n+s), n, N.le_trans(1n+Nat.double(s), 2n+Nat.double(s), Nat.double(1n+s), N.le_succ(1n+Nat.double(s)), L.subst(Nat, z => {Nat.is_le(2n+Nat.double(s), z) == True{} : Bool}, Nat.add(2n, Nat.double(s)), Nat.double(1n+s), Equal.sym(Nat, Nat.double(1n+s), Nat.add(2n, Nat.double(s)), N.double_succ(s)), N.le_refl(2n+Nat.double(s)))), h1)
65      +h3 = N.le_trans(Nat.double(s), 1n+Nat.double(s), n, N.le_succ(Nat.double(s)), h2)
66      +c = N.le_trans(S.choose(n, i), S.choose(n, s), S.choose(n, 1n+s), cmono_d(n, i, dp, h3), cstep(n, s, h2))
67      L.subst(Nat, z => {Nat.is_le(S.choose(n, i), S.choose(n, z)) == True{} : Bool}, 1n+s, Nat.add(i, 1n+dp), Equal.sym(Nat, Nat.add(i, 1n+dp), 1n+s, es), c)