Limbs.dm256: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs
Lines 177-181 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&start_line=177&end_line=181

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M

# n == (n mod 256) + 2^8 (n div 256)
def dm256(+n: Nat) -> {Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))) == n : Nat}:
  +e = Equal.sym(Nat, n, Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), NR.dm_eq(255n, n))
  +e2 = Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), M.cong_r(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n)), Nat.mul(Nat.div(n, 256n), 256n), Equal.sym(Nat, Nat.mul(Nat.div(n, 256n), 256n), C.shift(8n, Nat.div(n, 256n)), m256(Nat.div(n, 256n)))), NA.add_comm(Nat.mod(n, 256n), Nat.mul(Nat.div(n, 256n), 256n)))
  Equal.trans(Nat, Nat.add(Nat.mod(n, 256n), C.shift(8n, Nat.div(n, 256n))), Nat.add(Nat.mul(Nat.div(n, 256n), 256n), Nat.mod(n, 256n)), n, e2, e)

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=m256
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift