def lo_le
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/limbs.bend:189
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as Limbs
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
189def lo_le(+s: U32) -> {Nat.is_le(v(U32.mod(s, 256)), 255n) == True{} : Bool}:
190 %Equal.sym(Nat, v(U32.mod(s, 256)), Nat.mod(v(s), 256n), mod256(s)) : {Nat.is_le(_, 255n) == True{} : Bool}
191 N.lt_succ_le(Nat.mod(v(s), 256n), 255n, NR.dm_lt(255n, v(s)))