def rn_val

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

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

120# ((r + P - (c_n mod P)) mod P + c_p) mod P = (r + N) mod P
121def 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}:
122  +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))
123  %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}
124  %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}
125  %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}
126  {==}