def dmono

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

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/logic.bend as L
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

405def dmono(+n: Nat, +j: Nat, +d: Nat, +h: {Nat.is_le(Nat.add(j, d), n) == True{} : Bool}) -> {Nat.is_le(S.desc(n, j), S.desc(n, Nat.add(j, d))) == True{} : Bool}:
406  match d:
407    case 0n:
408      L.subst(Nat, z => {Nat.is_le(S.desc(n, j), S.desc(n, z)) == True{} : Bool}, j, Nat.add(j, 0n), Equal.sym(Nat, Nat.add(j, 0n), j, N.add_zero(j)), N.le_refl(S.desc(n, j)))
409    case 1n+ +dp:
410      +s = Nat.add(j, dp)
411      +es = NA.add_succ(j, dp)
412      +h1 = L.subst(Nat, z => {Nat.is_le(z, n) == True{} : Bool}, Nat.add(j, 1n+dp), 1n+s, es, h)
413      +hs = N.lt_le_trans(s, 1n+s, n, N.lt_succ(s), h1)
414      +c = N.le_trans(S.desc(n, j), S.desc(n, s), S.desc(n, 1n+s), dmono(n, j, dp, N.lt_le(s, n, hs)), dstep(n, s, hs))
415      L.subst(Nat, z => {Nat.is_le(S.desc(n, j), S.desc(n, z)) == True{} : Bool}, 1n+s, Nat.add(j, 1n+dp), Equal.sym(Nat, Nat.add(j, 1n+dp), 1n+s, es), c)