def comp1_o

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/negate.bend:100

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/src/crypto/secp256k1/limbs.bend as L

100def comp1_o(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.add(Nat.add(L.comp1(x), x), one) == C.shift(16n, one) : Nat}:
101  %Equal.sym(Nat, one, 1n, h1) : {Nat.add(Nat.add(L.comp1(x), x), _) == C.shift(16n, one) : Nat}
102  comp1_v(one, h1, x, hx)