def cn_ge

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:42

import Base
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/spec/lib/common.bend as C
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/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as B2
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend as K

42def cn_ge(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(C.shift(128n, one), FS.cn(one)) == True{} : Bool}:
43  %Equal.sym(Nat, FS.cn(one), Nat.add(FS.digits(one, K.cn8()), LV.pos(8n, one)), K.cn_split(one, h1)) : {Nat.is_le(C.shift(128n, one), _) == True{} : Bool}
44  %Equal.sym(Nat, LV.pos(8n, one), C.shift(128n, one), B2.pos_shift(8n, one)) : {Nat.is_le(C.shift(128n, one), Nat.add(FS.digits(one, K.cn8()), _)) == True{} : Bool}
45  %Equal.sym(Nat, Nat.add(FS.digits(one, K.cn8()), C.shift(128n, one)), Nat.add(C.shift(128n, one), FS.digits(one, K.cn8())), NA.add_comm(FS.digits(one, K.cn8()), C.shift(128n, one))) : {Nat.is_le(C.shift(128n, one), _) == True{} : Bool}
46  N.le_add_right(C.shift(128n, one), FS.digits(one, K.cn8()))