Nat.div2_pow2: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as Nat
Lines 531-533 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&start_line=531&end_line=533

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

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

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=div2_double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=pow2