Limbs.hi_lt: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs
Lines 193-203 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&start_line=193&end_line=203

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

# (s div 256) < 2^k when s < 2^(k + 8)
def hi_lt(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +s: U32, +h: {Nat.is_lt(v(s), WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}) -> {Nat.is_lt(v(U32.div(s, 256)), WD.sc(k, one)) == True{} : Bool}:
  %Equal.sym(Nat, v(U32.div(s, 256)), Nat.div(v(s), 256n), div256(s)) : {Nat.is_lt(_, WD.sc(k, one)) == True{} : Bool}
  +n = v(s)
  +q = Nat.div(n, 256n)
  +r = Nat.mod(n, 256n)
  +e = NR.dm_eq(255n, n)
  +h2 = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(Nat.add(k, 8n), one)) == True{} : Bool}, n, Nat.add(Nat.mul(q, 256n), r), e, h)
  +h3 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), z) == True{} : Bool}, WD.sc(Nat.add(k, 8n), one), WD.sc(k, WD.sc(8n, one)), AR.sc_idx(k, 8n, one), h2)
  +h4 = L.subst(Nat, z => {Nat.is_lt(Nat.add(Nat.mul(q, 256n), r), WD.sc(k, z)) == True{} : Bool}, WD.sc(8n, one), 256n, Equal.sym(Nat, 256n, WD.sc(8n, one), k256(one, h1)), h3)
  AR.quot_lt(k, one, h1, q, 256n, r, h4)

Uses (18):
  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=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=div256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=k256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=quot_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend&name=sc_idx
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq