def div2_pow2

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:531

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC

531# 2^(1+r) / 2 = 2^r
532def div2_pow2(+r: Nat) -> {Nat.div(SC.pow2(1n+r), 2n) == SC.pow2(r) : Nat}:
533  div2_double(SC.pow2(r))