def rn_cond

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

import Base

145# for r < N < P: (r + N) mod P >= N exactly when r + N < P
146def rn_cond(+r: Nat, +nn: Nat, +pp: Nat, +hr: {Nat.is_lt(r, nn) == True{} : Bool}, +hn: {Nat.is_lt(nn, 1n+pp) == True{} : Bool}, c: Bool, +hc: {Nat.is_lt(Nat.add(r, nn), 1n+pp) == c : Bool}) -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == c : Bool}:
147  match c:
148    case True{}:
149      rc_true(r, nn, pp, hc)
150    case False{}:
151      rc_false(r, nn, pp, hr, hn, hc)