def rc_false

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

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/crypto/secp256k1/ineq.bend as I

133def rc_false(+r: Nat, +nn: Nat, +pp: Nat, +hr: {Nat.is_lt(r, nn) == True{} : Bool}, +hn: {Nat.is_lt(nn, 1n+pp) == True{} : Bool}, +h: {Nat.is_lt(Nat.add(r, nn), 1n+pp) == False{} : Bool}) -> {Bool.not(Nat.is_lt(Nat.mod(Nat.add(r, nn), 1n+pp), nn)) == False{} : Bool}:
134  +x = Nat.add(r, nn)
135  +le1 = N.not_lt_le(x, 1n+pp, h)
136  +sa = N.sub_add(x, 1n+pp, le1)
137  +rp = N.lt_trans(r, nn, 1n+pp, hr, hn)
138  +he = N.sub_lt(x, 1n+pp, 1n+pp, le1, I.lt_le_add(r, nn, 1n+pp, 1n+pp, rp, N.lt_le(nn, 1n+pp, hn)))
139  +hen = N.sub_lt(x, 1n+pp, nn, le1, N.lt_add_r2(r, 1n+pp, nn, rp))
140  %Equal.sym(Nat, Nat.add(r, nn), Nat.add(1n+pp, Nat.sub(Nat.add(r, nn), 1n+pp)), Equal.sym(Nat, Nat.add(1n+pp, Nat.sub(Nat.add(r, nn), 1n+pp)), Nat.add(r, nn), sa)) : {Bool.not(Nat.is_lt(Nat.mod(_, 1n+pp), nn)) == False{} : Bool}
141  %Equal.sym(Nat, Nat.mod(Nat.add(1n+pp, Nat.sub(Nat.add(r, nn), 1n+pp)), 1n+pp), Nat.sub(Nat.add(r, nn), 1n+pp), mod_p1(pp, Nat.sub(Nat.add(r, nn), 1n+pp), he)) : {Bool.not(Nat.is_lt(_, nn)) == False{} : Bool}
142  %Equal.sym(Bool, Nat.is_lt(Nat.sub(Nat.add(r, nn), 1n+pp), nn), True{}, hen) : {Bool.not(_) == False{} : Bool}
143  {==}