def ell_valo
bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar3.bend:44
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar3.bend as Scalar3
import Base
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
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/ed25519/adc.bend as AD
44def ell_valo(+one: Nat) -> {K.valo(one, ESC.ell()) == SE.ell(one) : Nat}:
45 AD.valo_u(one, ESC.ell())