Pdec.hv_p: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend as Pdec
Lines 35-40 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend&start_line=35&end_line=40

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend as FZ
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M3

# y >= p exactly when the carry of y + 2^256 - p is not 0
def hv_p(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}) -> {Nat.add(K.valo(one, F.comp_p()), 1n+pp) == SC.T(one) : Nat}:
  +P = {1n+pp : Nat}
  +e1 = M3.cong_l(K.valo(one, F.comp_p()), Nat.add(P, 38n), P, FZ.comp_p_val(one, h1, pp, hP))
  +e2 = Equal.trans(Nat, Nat.add(Nat.add(P, 38n), P), Nat.add(P, Nat.add(38n, P)), Nat.add(Nat.add(P, P), 38n), NA.add_assoc(P, 38n, P), Equal.trans(Nat, Nat.add(P, Nat.add(38n, P)), Nat.add(P, Nat.add(P, 38n)), Nat.add(Nat.add(P, P), 38n), M3.cong_r(P, Nat.add(38n, P), Nat.add(P, 38n), NA.add_comm(38n, P)), Equal.sym(Nat, Nat.add(Nat.add(P, P), 38n), Nat.add(P, Nat.add(P, 38n)), NA.add_assoc(P, P, 38n))))
  Equal.trans(Nat, Nat.add(K.valo(one, F.comp_p()), P), Nat.add(Nat.add(P, 38n), P), SC.T(one), e1, Equal.trans(Nat, Nat.add(Nat.add(P, 38n), P), Nat.add(Nat.add(P, P), 38n), SC.T(one), e2, Equal.sym(Nat, SC.T(one), Nat.add(Nat.add(P, P), 38n), FZ.t_val(one, h1, pp, hP))))

Uses (14):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend&name=valo
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend&name=comp_p_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/freeze.bend&name=t_val
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend&name=T
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=comp_p