Prec.rc0: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Prec
Lines 140-148 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&start_line=140&end_line=148

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend as ES
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend as E
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/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend as SL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend as RC

def rc0(+one: Nat, +h1: {one == 1n : Nat}, +z: List<&2, Nat>, +hz: {FS.reduced(one, FS.order(one), z) == True{} : Bool}, +r: List<&2, Nat>, +hr: {FS.reduced(one, FS.order(one), r) == True{} : Bool}, +s: List<&2, Nat>, +hs: {FS.reduced(one, FS.order(one), s) == True{} : Bool}) -> {E.recover_ok(z, r, s, 0n, True{}) == ES.recover_ok(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, True{}) : Maybe<&2, List<&2, U32>>}:
  %Equal.sym(List<&2, Nat>, L.select(0n, E.rn_fe(r), r), r, SL.sel0(one, 16n, E.rn_fe(r), r, SL.l16(one, E.rn_fe(r), x1_r(one, h1, r, hr)), SL.sl16(one, r, hr))) : {E.recover_x(z, r, s, 0n, _, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), _), Nat.is_lt(Nat.add(FS.value(one, r), Nat.mul(0n, FS.order(one))), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, Nat.mul(0n, FS.order(one)), 0n, zmul(FS.order(one))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, Nat.add(FS.value(one, r), 0n), Nat.is_lt(Nat.add(FS.value(one, r), _), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, _, Nat.is_lt(Nat.add(FS.value(one, r), 0n), FS.prime(one))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, Nat.add(FS.value(one, r), 0n), FS.value(one, r), N.add_zero(FS.value(one, r))) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), Nat.is_lt(_, FS.prime(one))) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Nat, FS.prime(one), 1n+K.pp(one), K.prime_eq(one, h1)) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), Nat.is_lt(FS.value(one, r), _)) : Maybe<&2, List<&2, U32>>}
  %Equal.sym(Bool, Nat.is_lt(FS.value(one, r), 1n+K.pp(one)), True{}, r_lt_pp(one, h1, r, hr)) : {E.recover_x(z, r, s, 0n, r, True{}) == ES.recover_x_if(one, FS.value(one, z), FS.value(one, r), FS.value(one, s), 0n, FS.value(one, r), _) : Maybe<&2, List<&2, U32>>}
  rxg(one, h1, z, hz, r, hr, s, hs, 0n, r, rp_red(one, h1, r, hr), FS.value(one, r), Equal.sym(Nat, Nat.mod(FS.value(one, r), 1n+K.pp(one)), FS.value(one, r), RC.mod_small(K.pp(one), FS.value(one, r), r_lt_pp(one, h1, r, hr))), True{}, r_lt_pp(one, h1, r, hr))

Uses (32):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=pp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/consts.bend&name=prime_eq
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=r_lt_pp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=rp_red
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=rxg
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=x1_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend&name=zmul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/rconst.bend&name=mod_small
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=l16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sel0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/sel.bend&name=sl16
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=recover_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/ecdsa.bend&name=recover_x_if
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=order
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=prime
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=reduced
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=recover_ok
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=recover_x
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/ecdsa.bend&name=rn_fe
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=select