def mod_small

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:94

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

94# x mod P = x for x < P
95def mod_small(+pp: Nat, +x: Nat, +h: {Nat.is_lt(x, 1n+pp) == True{} : Bool}) -> {Nat.mod(x, 1n+pp) == x : Nat}:
96  NR.mod_of(0n, pp, x, h)