Rconst.mod_p1: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as Rconst
Lines 98-101 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&start_line=98&end_line=101

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

# (P + e) mod P = e for e < P
def 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}:
  %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}
  NR.mod_of(1n, pp, e, h)

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=m1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_of