Rconst.cn_ge: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as Rconst
Lines 42-46 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&start_line=42&end_line=46

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

def cn_ge(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(C.shift(128n, one), FS.cn(one)) == True{} : Bool}:
  %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}
  %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}
  %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}
  N.le_add_right(C.shift(128n, one), FS.digits(one, K.cn8()))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=pos_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=cn8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=cn_split
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=cn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=digits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift