def half_dbl1

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

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

409def half_dbl1(+y: Nat) -> {C.half(1n+Nat.double(y)) == y : Nat}:
410  WI.half_dbl(1n, y)