Rconst.rc_false: 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 133-143 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=133&end_line=143

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

def 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}:
  +x = Nat.add(r, nn)
  +le1 = N.not_lt_le(x, 1n+pp, h)
  +sa = N.sub_add(x, 1n+pp, le1)
  +rp = N.lt_trans(r, nn, 1n+pp, hr, hn)
  +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)))
  +hen = N.sub_lt(x, 1n+pp, nn, le1, N.lt_add_r2(r, 1n+pp, nn, rp))
  %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}
  %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}
  %Equal.sym(Bool, Nat.is_lt(Nat.sub(Nat.add(r, nn), 1n+pp), nn), True{}, hen) : {Bool.not(_) == False{} : Bool}
  {==}

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  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=lt_le_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=mod_p1
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_add_r2
  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/lib/nat.bend&name=lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=not_lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_lt