def shr16
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrnimport Base
155# the 16-bit split of the limb code
156def shr16(+x: U32) -> {U32.shrn(x, 16n) == U32.div(x, 65536) : U32}:
157 shrn_div(x, 16n, {==})
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/shrn.bend as Shrnimport Base
155# the 16-bit split of the limb code
156def shr16(+x: U32) -> {U32.shrn(x, 16n) == U32.div(x, 65536) : U32}:
157 shrn_div(x, 16n, {==})