Negate.hi_byte_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend as Negate
Lines 54-63 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&start_line=54&end_line=63

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/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend as R

# x < 2^16: x div 256 < 256
def hi_byte_lt(+one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +hx: {Nat.is_lt(x, C.shift(16n, one)) == True{} : Bool}) -> {Nat.is_lt(Nat.div(x, 256n), 256n) == True{} : Bool}:
  +bq = C.shift(8n, one)
  +hi = Nat.div(x, 256n)
  +le = I.le_subst_r(Nat.mul(hi, 256n), Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), x, Equal.sym(Nat, x, Nat.add(Nat.mul(hi, 256n), Nat.mod(x, 256n)), NR.dm_eq(255n, x)), N.le_add_right(Nat.mul(hi, 256n), Nat.mod(x, 256n)))
  +le2 = I.le_subst_l(Nat.mul(hi, 256n), Nat.mul(hi, bq), x, Equal.cong(Nat, Nat, z => Nat.mul(hi, z), 256n, bq, Equal.sym(Nat, bq, 256n, LV.b8(one, h1))), le)
  +s1 = N.le_lt_trans(Nat.mul(hi, bq), x, C.shift(16n, one), le2, hx)
  +s2 = I.lt_subst_r(Nat.mul(hi, bq), C.shift(16n, one), Nat.mul(bq, bq), Equal.sym(Nat, Nat.mul(bq, bq), C.shift(16n, one), bb_sq(one, h1)), s1)
  +s3 = R.mul_lt_cancel(bq, hi, bq, s2, Nat.is_lt(hi, bq), {==})
  I.lt_subst_r(hi, bq, 256n, LV.b8(one, h1), s3)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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/ineq.bend&name=le_subst_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=le_subst_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=lt_subst_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=b8
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/negate.bend&name=bb_sq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/reduce.bend&name=mul_lt_cancel
  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/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift