def pm_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/math/random/uint64n.bend:164

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

164def pm_lt(+m: Nat, +one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_lt(SR.pow2mod(64n, 1n+m), 1n+m) == True{} : Bool}:
165  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{},
166    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)),
167    AR.dm_lt(m, C.shift(64n, one)))