proofs/crypto/ed25519/scalar.bend checks

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../spec/crypto/curve25519/x25519.bend as SX
import ../../../src/crypto/curve25519/field.bend as F
import ../../../src/crypto/curve25519/x25519.bend as X
import ../../../src/crypto/ed25519/scalar.bend as ESC
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/u32.bend as U
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/typed/width.bend as WI
import ../curve25519/num.bend as M
import ../curve25519/limbs.bend as LM
import ../curve25519/poly.bend as PL
import ../curve25519/fold.bend as FD
import ../curve25519/reduce.bend as RD
import ../curve25519/consts.bend as K
import ../curve25519/fieldops.bend as FO
import ../curve25519/freeze.bend as FZ
import ../curve25519/cong.bend as G
import ../curve25519/xbits.bend as XB