def sub1_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/bitsv.bend:209

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

209def sub1_lt(b: Nat) -> {Nat.is_lt(Nat.sub(1n, b), 2n) == True{} : Bool}:
210  match b:
211    case 0n:
212      {==}
213    case 1n+k:
214      %Equal.sym(Nat, Nat.sub(0n, k), 0n, NR.zsub(k)) : {Nat.is_lt(_, 2n) == True{} : Bool}
215      {==}