def r_zero
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pcodec.bend:51
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as Pcodec
import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
51def r_zero(+pp: Nat) -> RL.R(pp, F.zero(), 0n):
52 ({==}, G.c_refl(pp, 0n))