Fieldops.eight_p_gea: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as Fieldops
Lines 165-166 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&start_line=165&end_line=166

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F

def eight_p_gea() -> {gea(F.eight_p(), 255n) == True{} : Bool}:
  {==}

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=gea
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=eight_p