Rconst.rn_val: 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 120-126 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=120&end_line=126

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend as I

# ((r + P - (c_n mod P)) mod P + c_p) mod P = (r + N) mod P
def rn_val(+r: Nat, +nn: Nat, +pp: Nat, +cn: Nat, +cp: Nat, +hs: {Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat}, +hcn: {Nat.is_lt(cn, 1n+pp) == True{} : Bool}) -> {Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), Nat.mod(cn, 1n+pp)), 1n+pp), cp), 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat}:
  +hl = N.le_trans(cn, 1n+pp, Nat.add(r, 1n+pp), N.lt_le(cn, 1n+pp, hcn), I.le_add_l(r, 1n+pp))
  %Equal.sym(Nat, Nat.mod(cn, 1n+pp), cn, mod_small(pp, cn, hcn)) : {Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), _), 1n+pp), cp), 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat}
  %Equal.sym(Nat, Nat.mod(Nat.add(Nat.mod(Nat.sub(Nat.add(r, 1n+pp), cn), 1n+pp), cp), 1n+pp), Nat.mod(Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp), 1n+pp), NR.mod_add_l(pp, Nat.sub(Nat.add(r, 1n+pp), cn), cp)) : {_ == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat}
  %Equal.sym(Nat, Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp), Nat.add(r, nn), rn_sum(r, nn, pp, cn, cp, hs, hl)) : {Nat.mod(_, 1n+pp) == Nat.mod(Nat.add(r, nn), 1n+pp) : Nat}
  {==}

Uses (13):
  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.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/ineq.bend&name=le_add_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=mod_small
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=rn_sum
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=mod_add_l