U32div.sub32: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend as U32div
Lines 70-77 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&start_line=70&end_line=77

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD

def sub32(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +b: U32, +d: Nat, +e: {Nat.add(v(x), WD.sc(32n, one)) == Nat.add(d, v(b)) : Nat}, +hd: {Nat.is_lt(d, WD.sc(32n, one)) == True{} : Bool}) -> {v(U32.sub(x, b)) == d : Nat}:
  match x b:
    case U32{+xw} U32{+bw}:
      +e2 = Equal.trans(Nat, Nat.add(WD.uw(32n, xw), WD.sc(32n, one)), Nat.add(v(U32{xw}), WD.sc(32n, one)), Nat.add(d, WD.uw(32n, bw)),
        Equal.cong(Nat, Nat, z => Nat.add(z, WD.sc(32n, one)), WD.uw(32n, xw), v(U32{xw}), Equal.sym(Nat, v(U32{xw}), WD.uw(32n, xw), vw(xw))),
        Equal.trans(Nat, Nat.add(v(U32{xw}), WD.sc(32n, one)), Nat.add(d, v(U32{bw})), Nat.add(d, WD.uw(32n, bw)), e, Equal.cong(Nat, Nat, z => Nat.add(d, z), v(U32{bw}), WD.uw(32n, bw), vw(bw))))
      %Equal.sym(Nat, v(U32{Word.sub(32n, xw, bw)}), WD.uw(32n, Word.sub(32n, xw, bw)), vw(Word.sub(32n, xw, bw))) : {_ == d : Nat}
      WD.sub_wrap(32n, one, h1, xw, bw, d, e2, hd)

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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32div.bend&name=vw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sub_wrap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw