PROOFMul.wm.low2: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_mul.bend as PROOFMul
Lines 159-161 of bend-osdev-word64@0.1.1.0/PROOF_mul.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_mul.bend&start_line=159&end_line=161

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

# lo + 2^h hi < 2^n for lo, hi < 2^h
def wm.low2(+h: Nat, +n: Nat, +x: Nat, +y: Nat, +en: {Nat.add(h, h) == n : Nat}, +hx: {Nat.is_lt(x, U.U32Nat.dbl(h, 1n)) == True{} : Bool}, +hy: {Nat.is_lt(y, U.U32Nat.dbl(h, 1n)) == True{} : Bool}) -> {Nat.is_lt(Nat.add(x, U.U32Nat.dbl(h, y)), U.U32Nat.dbl(n, 1n)) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_lt(Nat.add(x, U.U32Nat.dbl(h, y)), U.U32Nat.dbl(n, 1n)), Nat.is_lt(Nat.add(x, U.U32Nat.dbl(h, y)), P.wv.Q(h, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(Nat.add(x, U.U32Nat.dbl(h, y)), zz), U.U32Nat.dbl(n, 1n), P.wv.Q(h, 1n), Equal.sym(Nat, P.wv.Q(h, 1n), U.U32Nat.dbl(n, 1n), Equal.sym(Nat, U.U32Nat.dbl(n, 1n), U.U32Nat.dbl(h, U.U32Nat.dbl(h, 1n)), wm.fn(h, n, 1n, en)))), P.wv.val_lt2(h, x, y, hx, hy))

Uses (11):
  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=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_mul.bend&name=wm.fn
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.Q
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wv.val_lt2