proofs/crypto/secp256k1/fieldops.bend checks

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/secp256k1/field.bend as FS
import ../../../src/crypto/secp256k1/limbs.bend as L
import ../../../src/crypto/secp256k1/field.bend as F
import ../../lib/nat.bend as N
import ../../lib/logic.bend as Lg
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ./limbs.bend as LV
import ./fprot.bend as FR
import ./ineq.bend as I
import ./bounds.bend as B
import ./reducek.bend as RK
import ./consts.bend as K
import ./negate.bend as NG
import ./listops.bend as LO