def cong_mod

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/num.bend:28

import Base

28def cong_mod(+m: Nat, +x: Nat, +y: Nat, +e: {x == y : Nat}) -> {Nat.mod(x, m) == Nat.mod(y, m) : Nat}:
29  Equal.cong(Nat, Nat, t => Nat.mod(t, m), x, y, e)