def tests_mul_over
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32laws.bend:265
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32laws.bend as U32laws
import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/instances.bend as SI
import bend-collections-laws-math@1.0.0.0/spec/math/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
265def tests_mul_over(+a: U32, +b: U32) -> SI.Tests.mul_over(~U32, ~I.u32_is, ~SG.u32_val, 32n, a, b):
266 Equal.cong(Bool, Bool, t => Bool.not(t), U32.is_zero(X.hi(X.mul32(a, b))), C.fits(32n, Nat.mul(v(a), v(b))), mul_over_k(32n, {==}, a, b))