def sub_succ_r

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/w64sqrt.bend:164

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

164# b - a == 1 + (b - (a + 1)) for a < b
165def sub_succ_r(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.sub(b, a) == 1n+Nat.sub(b, 1n+a) : Nat}:
166  match b:
167    case 0n:
168      Empty.absurd({Nat.sub(0n, a) == 1n+Nat.sub(0n, 1n+a) : Nat}, N.lt_zero_absurd(a, h))
169    case 1n+ +bp:
170      N.sub_succ_left(bp, a, N.lt_succ_le(a, bp, h))