def vb

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32div.bend:64

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

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