def mul_m
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fix64.bend:280
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fix64.bend as Fix64
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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/fixgen.bend as G
280def mul_m(+mp: Nat, +hp: {C.pow2(64n) == 1n+mp : Nat}, +x: WU.U64, +y: WU.U64) -> {SG.u64_val(X.mul(x, y)) == Nat.mod(Nat.mul(SG.u64_val(x), SG.u64_val(y)), 1n+mp) : Nat}:
281 Equal.trans(Nat, SG.u64_val(X.mul(x, y)), C.low(64n, Nat.mul(SG.u64_val(x), SG.u64_val(y))), Nat.mod(Nat.mul(SG.u64_val(x), SG.u64_val(y)), 1n+mp), WA.mul_value(x, y), G.low_mod(64n, Nat.mul(SG.u64_val(x), SG.u64_val(y)), mp, hp))