def mul_low
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix32.bend:63
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix32.bend as Fix32
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/generic.bend as SG
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sh.bend as SH
63def mul_low(+x: U32, +y: U32) -> {SG.u32_val(U32.mul(x, y)) == C.low(32n, Nat.mul(SG.u32_val(x), SG.u32_val(y))) : Nat}:
64 SH.mul_low(x, y)