proofs/math/typed/f64mulv.bend checks

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
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/lemmas/proofs/nat_algebra.bend as NA
import ./width.bend as WW
import ../../lib/word.bend as WD
import ./w64sh.bend as SH
import ./u32laws.bend as LW
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64norm.bend as NM
import ./f64mexp.bend as EX
import ./f64mul.bend as MU
import ./f64mulf.bend as MF
import ./f64mulc.bend as MC