Uint64n.pm_one: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
Lines 75-78 of bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&start_line=75&end_line=78

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/spec/math/random/rand.bend as SR
import bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend as LE

# pow2mod through a symbolic one (2^64 is never a closed term)
def pm_one(+w: Nat, +m: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {SR.pow2mod(w, 1n+m) == Nat.mod(C.shift(w, one), 1n+m) : Nat}:
  %Equal.sym(Nat, one, 1n, h1) : {SR.pow2mod(w, 1n+m) == Nat.mod(C.shift(w, _), 1n+m) : Nat}
  LE.pm(w, m)

Uses (6):
  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.mod
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/lemire.bend&name=pm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/math/random/rand.bend&name=pow2mod