~/jendhub

def mod_sh

bend-collections-laws-math@1.0.0.0 · proofs/math/random/fround.bend:217

import bend-collections-laws-math@1.0.0.0/proofs/math/random/fround.bend as Fround
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW

217def mod_sh(+k: Nat, +x: Nat) -> {Nat.mod(C.shift(1n+k, x), 2n) == 0n : Nat}:
218  WW.odd_limb(k, 0n, x)

Uses (4)

Used by (1)