def cn_mono

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

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

77def cn_mono(+m: Nat, +j: Nat) -> {Nat.is_le(S.choose(m, j), S.choose(1n+m, j)) == True{} : Bool}:
78  match m j:
79    case 0n 0n:
80      {==}
81    case 0n 1n+jp:
82      N.zero_le(S.choose(1n, 1n+jp))
83    case 1n+mp 0n:
84      {==}
85    case 1n+ +mp 1n+ +jp:
86      +a = S.choose(1n+mp, jp)
87      +b = S.choose(1n+mp, 1n+jp)
88      L.subst(Nat, z => {Nat.is_le(b, z) == True{} : Bool}, Nat.add(b, a), Nat.add(a, b), N.add_comm(b, a), N.le_add_right(b, a))