Uint64n.pm_lt: 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 164-167 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=164&end_line=167

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/natural/arith.bend as AR

def pm_lt(+m: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}:
  Equal.trans(Bool, Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m), Nat.is_lt(Nat.mod(C.shift(64n, one), 1n+m), 1n+m), True{},
    Equal.cong(Nat, Bool, z => Nat.is_lt(z, 1n+m), SR.pow2mod(64n, 1n+m), Nat.mod(C.shift(64n, one), 1n+m), pm_one(64n, m, one, h1)),
    AR.dm_lt(m, C.shift(64n, one)))

Uses (10):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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.is_lt
  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/natural/arith.bend&name=dm_lt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/random/uint64n.bend&name=pm_one
  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