def sub_lt_succ

bend-collections-laws-crypto@1.0.0.0 · proofs/math/natural/fact.bend:92

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N

92# j < n gives n - j == 1 + (n - (1 + j))
93def sub_lt_succ(+n: Nat, +j: Nat, +h: {Nat.is_lt(j, n) == True{} : Bool}) -> {Nat.sub(n, j) == 1n+Nat.sub(n, 1n+j) : Nat}:
94  match n j:
95    case 0n j0:
96      Empty.absurd({Nat.sub(0n, j0) == 1n+Nat.sub(0n, 1n+j0) : Nat}, N.lt_zero_absurd(j0, h))
97    case 1n+ +np 0n:
98      Equal.sym(Nat, 1n+Nat.sub(np, 0n), 1n+np, N.succ_cong(Nat.sub(np, 0n), np, N.sub_zero(np)))
99    case 1n+ +np 1n+ +jp:
100      sub_lt_succ(np, jp, h)