def rn_sum

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

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

114# with P + c_p = N + c_n and c_n <= r + P: (r + P - c_n) + c_p = r + N
115def rn_sum(+r: Nat, +nn: Nat, +pp: Nat, +cn: Nat, +cp: Nat, +hs: {Nat.add(1n+pp, cp) == Nat.add(nn, cn) : Nat}, +hl: {Nat.is_le(cn, Nat.add(r, 1n+pp)) == True{} : Bool}) -> {Nat.add(Nat.sub(Nat.add(r, 1n+pp), cn), cp) == Nat.add(r, nn) : Nat}:
116  +d = Nat.sub(Nat.add(r, 1n+pp), cn)
117  +sa = N.sub_add(Nat.add(r, 1n+pp), cn, hl)
118  NR.add_cancel(cn, Nat.add(d, cp), Nat.add(r, nn), rn_sum_c(r, nn, pp, cn, cp, hs, sa))