Bounds.lo16_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend as Bounds
Lines 47-50 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&start_line=47&end_line=50

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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR
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/ineq.bend as I

def lo16_lt(+one: Nat, +h1: {one == 1n : Nat}, +s: Nat) -> {Nat.is_lt(L.lo16(s), C.shift(16n, one)) == True{} : Bool}:
  %Equal.sym(Nat, Nat.mul(Nat.mod(Nat.div(s, 256n), 256n), 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n)), LV.m256(Nat.mod(Nat.div(s, 256n), 256n))) : {Nat.is_lt(Nat.add(Nat.mod(s, 256n), _), C.shift(16n, one)) == True{} : Bool}
  %Equal.sym(Nat, C.shift(16n, one), C.shift(8n, C.shift(8n, one)), Equal.sym(Nat, C.shift(8n, C.shift(8n, one)), C.shift(16n, one), SR.shift_shift(8n, 8n, one))) : {Nat.is_lt(Nat.add(Nat.mod(s, 256n), C.shift(8n, Nat.mod(Nat.div(s, 256n), 256n))), _) == True{} : Bool}
  I.digit_lt(8n, one, h1, Nat.mod(s, 256n), Nat.mod(Nat.div(s, 256n), 256n), C.shift(8n, one), mod256_lt(one, h1, s), mod256_lt(one, h1, Nat.div(s, 256n)))

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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/bounds.bend&name=mod256_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=digit_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=m256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=shift_shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=lo16