def bit_dbl0
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend as Lemireimport Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WI
400def bit_dbl0(+y: Nat) -> {C.bit(Nat.double(y)) == 0n : Nat}:
401 WI.bit_dbl(0n, y)