def c_eq

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as Cong

import Base

22def c_eq(+pp: Nat, +a: Nat, +b: Nat, +e: {a == b : Nat}) -> ceq(pp, a, b):
23  Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+pp), a, b, e)

Uses (4)