PROOFBits.wb.mlt: def of bend-osdev-word64@0.1.1.0
Import: import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as PROOFBits
Lines 140-142 of bend-osdev-word64@0.1.1.0/PROOF_bits.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&start_line=140&end_line=142

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
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

# nothing is above the mask of all n bits
def wb.mlt(+n: Nat, +w: Word(n)) -> {Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)) == False{} : Bool}:
  Equal.trans(Bool, Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)), Nat.is_lt(Word.to_nat(n, U.U32Word.mask(n, n)), Word.to_nat(n, w)), False{}, Equal.cong(Cmp, Bool, zz => Cmp.is_lt(zz), Word.cmp(n, U.U32Word.mask(n, n), w), Nat.cmp(Word.to_nat(n, U.U32Word.mask(n, n)), Word.to_nat(n, w)), UL.word_cmp_value(n, U.U32Word.mask(n, n), w)), P.wn.le_not_lt(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n)), Equal.trans(Bool, Nat.is_le(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), True{}, Equal.sym(Bool, Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_le(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n))), wb.lts(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n)))), Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(Word.to_nat(n, w), zz), 1n+Word.to_nat(n, U.U32Word.mask(n, n)), U.U32Nat.dbl(n, 1n), UL.word_mask_value(n, n, UL.nat_le_refl(n))), UL.word_value_lt(n, w)))))

Uses (21):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_lt
  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.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_refl
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_cmp_value
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_mask_value
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_value_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-u32@0.1.0.0/u32.bend&name=U32Word.mask
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/PROOF_bits.bend&name=wb.lts
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.0/proof_value.bend&name=wn.le_not_lt