def mod2_lt

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/penc.bend:114

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR

114def mod2_lt(+v: Nat) -> {Nat.is_lt(Nat.mod(v, 2n), 2n) == True{} : Bool}:
115  NR.dm_lt(1n, v)