def mod_p1

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/rconst.bend:98

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

98# (P + e) mod P = e for e < P
99def mod_p1(+pp: Nat, +e: Nat, +h: {Nat.is_lt(e, 1n+pp) == True{} : Bool}) -> {Nat.mod(Nat.add(1n+pp, e), 1n+pp) == e : Nat}:
100  %Equal.sym(Nat, 1n+pp, Nat.mul(1n, 1n+pp), Equal.sym(Nat, Nat.mul(1n, 1n+pp), 1n+pp, m1(1n+pp))) : {Nat.mod(Nat.add(_, e), 1n+pp) == e : Nat}
101  NR.mod_of(1n, pp, e, h)