~/jendhub

def mod2_le

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:179

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

179def mod2_le(+a: Nat) -> {Nat.is_le(Nat.mod(a, 2n), 1n) == True{} : Bool}:
180  N.lt_succ_le(Nat.mod(a, 2n), 1n, NR.dm_lt(1n, a))

Uses (6)

Used by (1)