def red

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

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

160def red(+pp: Nat, +a: Nat) -> {Nat.mod(Nat.mod(a, 1n+pp), 1n+pp) == Nat.mod(a, 1n+pp) : Nat}:
161  NR.mod_mod(pp, a)