def c_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/cong.bend:25

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

25# the reduced value is congruent to the value
26def c_mod(+pp: Nat, +a: Nat) -> ceq(pp, Nat.mod(a, 1n+pp), a):
27  NR.mod_mod(pp, a)