Prime.prime_eq: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend as Prime
Lines 29-32 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend&start_line=29&end_line=32

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
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/lib/word.bend as WD

def prime_eq(+one: Nat, +h1: {one == 1n : Nat}) -> {FS.prime(one) == 1n+pp_of(one) : Nat}:
  +pp = pp_of(one)
  +e = Equal.cong(Nat, Nat, t => Nat.sub(t, 19n), WD.sc(255n, one), Nat.add(20n, pp), Equal.sym(Nat, Nat.add(20n, pp), WD.sc(255n, one), pp_sum(one, h1)))
  Equal.trans(Nat, Nat.sub(WD.sc(255n, one), 19n), Nat.sub(Nat.add(20n, pp), 19n), 1n+pp, e, N.add_sub_cancel(19n, 1n+pp))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend&name=pp_of
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend&name=pp_sum
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_sub_cancel
  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/spec/crypto/curve25519/field.bend&name=prime