def cn_red

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/secp256k1/prec.bend:102

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/src/crypto/secp256k1/ecdsa.bend as E
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as Lg
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/ineq.bend as I
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/rconst.bend as RC

102def cn_red(+one: Nat, +h1: {one == 1n : Nat}) -> {PT.red(one, E.cn_fe()) == True{} : Bool}:
103  +h = I.lt_subst_l(FS.cn(one), FS.value(one, E.cn_fe()), 1n+K.pp(one), Equal.sym(Nat, FS.value(one, E.cn_fe()), FS.cn(one), RC.cn_fe_v(one)), RC.cn_lt_p(one, h1))
104  Lg.and_intro(FS.limbs16(one, 16n, E.cn_fe()), Nat.is_lt(FS.value(one, E.cn_fe()), FS.prime(one)), RC.cn_fe_l(one, h1), to_p(one, h1, FS.value(one, E.cn_fe()), h))