def rq_v
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:54
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/prec.bend as Prec
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/secp256k1/curve.bend as CV
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/point.bend as P
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/crypto/secp256k1/point.bend as PT
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/paff.bend as PA
54def rq_v(+one: Nat, +h1: {one == 1n : Nat}, +q: P.Point, +hq: {PT.pred(one, q) == True{} : Bool}) -> {E.recover_q(q, P.is_inf(q)) == ES.recover_q(one, PT.pv(one, q)) : Maybe<&2, List<&2, U32>>}:
55 %Equal.sym(Bool, P.is_inf(q), CV.is_inf(PT.pv(one, q)), PA.is_inf_v(one, h1, q)) : {E.recover_q(q, _) == ES.recover_q(one, PT.pv(one, q)) : Maybe<&2, List<&2, U32>>}
56 rq_b(one, h1, q, hq, CV.is_inf(PT.pv(one, q)))