PROOFMul.wm.hl: def of bend-osdev-word64@0.1.1.1
Import: import bend-osdev-word64@0.1.1.1/PROOF_mul.bend as PROOFMul
Lines 81-82 of bend-osdev-word64@0.1.1.1/PROOF_mul.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.1/PROOF_mul.bend&start_line=81&end_line=82

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

def wm.hl(+k: Nat, +x: Nat, +K: Nat, +hx: {Nat.is_lt(x, U.U32Nat.dbl(k, K)) == True{} : Bool}) -> {Nat.is_lt(U.U32Nat.high(k, x), K) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_lt(U.U32Nat.high(k, x), K), Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), Nat.is_lt(U.U32Nat.high(k, x), K), UL.dbl_lt(k, U.U32Nat.high(k, x), K)), Equal.trans(Bool, Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x)))), True{}, Equal.sym(Bool, Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x)))), Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), U.U32Nat.dbl(k, K)), Equal.cong(Nat, Bool, zz => Nat.is_lt(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), zz), Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x))), U.U32Nat.dbl(k, K), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x))), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+x), U.U32Nat.dbl(k, K), Equal.trans(Nat, Nat.add(Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)), 1n+U.U32Nat.dbl(k, U.U32Nat.high(k, x))), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x)))), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+x), wr.m0(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x), k, U.U32Nat.high(k, x)), Equal.cong(Nat, Nat, zz => Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), 1n+zz), Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x))), x, UL.low_high(k, x))), UL.nat_lt_witness(x, U.U32Nat.dbl(k, K), hx)))), UL.nat_lt_add(U.U32Nat.dbl(k, U.U32Nat.high(k, x)), Nat.add(Nat.sub(U.U32Nat.dbl(k, K), 1n+x), U.U32Nat.low(k, x)))))

Uses (16):
  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=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.add
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_lt
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_high
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_witness
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.high
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.low
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/PROOF_mul.bend&name=wr.m0