Wrappers.div256: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend as Wrappers
Lines 161-162 of bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/wrappers.bend&start_line=161&end_line=162

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 WW

def div256(+n: Nat) -> {Nat.div(n, 256n) == C.high(8n, n) : Nat}:
  Equal.sym(Nat, C.high(8n, n), Nat.div(n, 256n), WW.high_div(8n, n, 255n, {==}))

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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-math@1.0.0.0/proofs/math/typed/width.bend&name=high_div
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high