def at_p

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/proof.bend:42

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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend as PR

42# a statement about p = 1 + pp, restated about FS.prime(one)
43def at_p(+one: Nat, +h1: {one == 1n : Nat}, -M: Nat -> Type, pf: M(1n+pp1(one))) -> M(FS.prime(one)):
44  L.subst(Nat, M, 1n+pp1(one), FS.prime(one), Equal.sym(Nat, FS.prime(one), 1n+pp1(one), PR.prime_eq(one, h1)), pf)