def half_dbl0

bend-collections-laws-math@1.0.0.0 · proofs/math/random/lemire.bend:403

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 WI

403def half_dbl0(+y: Nat) -> {C.half(Nat.double(y)) == y : Nat}:
404  WI.half_dbl(0n, y)