def w_succ
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/listops.bend:92
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/listops.bend as Listops
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B
92def w_succ(+one: Nat, +h1: {one == 1n : Nat}) -> {1n+Nat.sub(C.shift(16n, one), 1n) == C.shift(16n, one) : Nat}:
93 N.sub_add(C.shift(16n, one), 1n, N.lt_succ_le_succ(0n, C.shift(16n, one), B.pos_pos(one, h1, 1n)))