U32div.vb: 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 64-68 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=64&end_line=68

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

def vb(+one: Nat, +h1: {one == 1n : Nat}, +x: U32) -> {Nat.is_lt(v(x), WD.sc(32n, one)) == True{} : Bool}:
  match x:
    case U32{+w}:
      %Equal.sym(Nat, v(U32{w}), WD.uw(32n, w), vw(w)) : {Nat.is_lt(_, WD.sc(32n, one)) == True{} : Bool}
      WD.wb(32n, one, h1, w)

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  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=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=uw
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=wb