proofs/math/typed/u32mont.bend checks

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/w64.bend as SW
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/u32div.bend as UD
import ../../lib/lemmas/spec/numeric.bend as S
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ../natural/sqrtn.bend as SQ2
import ../u64/u64.bend as P64
import ./width.bend as WW
import ./u32laws.bend as LW
import ./w64add.bend as WA
import ./w64mul.bend as W64M
import ./w64sqrt.bend as W64S
import ./w64sh.bend as SH
import ./w64m128.bend as M128
import ./w64div.bend as W64D
import ./w64dm.bend as DM
import ./natlight.bend as AQ
import ./montnat.bend as MN
import ./u64mont.bend as UM