PROOFText.wsd.k2: def of bend-osdev-word64@0.1.1.1
Import: import bend-osdev-word64@0.1.1.1/PROOF_text.bend as PROOFText
Lines 171-173 of bend-osdev-word64@0.1.1.1/PROOF_text.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-word64@0.1.1.1/PROOF_text.bend&start_line=171&end_line=173

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-u32@0.1.0.0/LAWS_order.bend as UO

# 10 d + m = v < 2^h 10: d < 2^h
def wsd.k2(+h: Nat, +V: Nat, +Dd: Nat, +M: Nat, +edm: {Nat.add(Nat.mul(Dd, 10n), M) == V : Nat}, +hv: {Nat.is_lt(V, U.U32Nat.dbl(h, 10n)) == True{} : Bool}) -> {Nat.is_lt(Dd, U.U32Nat.dbl(h, 1n)) == True{} : Bool}:
  wsd.mlc(Dd, U.U32Nat.dbl(h, 1n), 10n, UO.nat_le_lt_trans(Nat.mul(Dd, 10n), V, Nat.mul(U.U32Nat.dbl(h, 1n), 10n), Equal.trans(Bool, Nat.is_le(Nat.mul(Dd, 10n), V), Nat.is_le(Nat.mul(Dd, 10n), Nat.add(M, Nat.mul(Dd, 10n))), True{}, Equal.sym(Bool, Nat.is_le(Nat.mul(Dd, 10n), Nat.add(M, Nat.mul(Dd, 10n))), Nat.is_le(Nat.mul(Dd, 10n), V), Equal.cong(Nat, Bool, zz => Nat.is_le(Nat.mul(Dd, 10n), zz), Nat.add(M, Nat.mul(Dd, 10n)), V, Equal.trans(Nat, Nat.add(M, Nat.mul(Dd, 10n)), Nat.add(Nat.mul(Dd, 10n), M), V, wr.t4(M, Dd), edm))), UL.nat_le_add(Nat.mul(Dd, 10n), M)), Equal.trans(Bool, Nat.is_lt(V, Nat.mul(U.U32Nat.dbl(h, 1n), 10n)), Nat.is_lt(V, U.U32Nat.dbl(h, 10n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(V, zz), Nat.mul(U.U32Nat.dbl(h, 1n), 10n), U.U32Nat.dbl(h, 10n), Equal.sym(Nat, U.U32Nat.dbl(h, 10n), Nat.mul(U.U32Nat.dbl(h, 1n), 10n), wr.t5(h))), hv)))

Uses (15):
  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_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=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS_order.bend&name=nat_le_lt_trans
  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.1/PROOF_text.bend&name=wr.t4
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/PROOF_text.bend&name=wr.t5
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/PROOF_text.bend&name=wsd.mlc