ProofU32.uq.hk0: def of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
Lines 397-399 of bend-osdev-algo@0.1.0.0/proof_u32.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&start_line=397&end_line=399

import Base

# the bound for the bits above the lowest, from the bound for the word
def uq.hk0(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(s2, q) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_lt(s2, q), Nat.is_lt(Nat.double(s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(s2), Nat.double(q)), Nat.is_lt(s2, q), uq.lt_dbl(s2, q)), uq.lt_rw(d, Nat.double(s2), Nat.double(q), Equal.sym(Nat, Nat.double(s2), d, e), h))

Uses (8):
  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=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.lt_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/proof_u32.bend&name=uq.lt_rw