def digits_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/consts.bend:153

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as LV
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B

153def digits_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +ys: List<&2, Nat>, +h: {FS.limbs16(one, k, ys) == True{} : Bool}) -> {Nat.is_lt(FS.digits(one, ys), LV.pos(k, one)) == True{} : Bool}:
154  %Equal.sym(Nat, FS.digits(one, ys), LV.ev(ys), LV.ev_value(one, h1, ys)) : {Nat.is_lt(_, LV.pos(k, one)) == True{} : Bool}
155  B.limbs_lt(one, h1, k, ys, h)