def hi16
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64mulimport Base
71def hi16(+x: U32, +c: U32) -> Nat:
72 v(U32.div(x, c))
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as W64mulimport Base
71def hi16(+x: U32, +c: U32) -> Nat:
72 v(U32.div(x, c))