def smul

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mulf.bend:49

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/proofs/math/typed/width.bend as WW

49def smul(+k: Nat, +j: Nat, +x: Nat, +y: Nat) -> {Nat.mul(C.shift(k, x), C.shift(j, y)) == C.shift(Nat.add(k, j), Nat.mul(x, y)) : Nat}:
50  Equal.trans(Nat, Nat.mul(C.shift(k, x), C.shift(j, y)), C.shift(k, Nat.mul(x, C.shift(j, y))), C.shift(Nat.add(k, j), Nat.mul(x, y)), WW.shift_mul_l(k, x, C.shift(j, y)), Equal.trans(Nat, C.shift(k, Nat.mul(x, C.shift(j, y))), C.shift(k, C.shift(j, Nat.mul(x, y))), C.shift(Nat.add(k, j), Nat.mul(x, y)), Equal.cong(Nat, Nat, z => C.shift(k, z), Nat.mul(x, C.shift(j, y)), C.shift(j, Nat.mul(x, y)), WW.shift_mul_r(j, x, y)), Equal.sym(Nat, C.shift(Nat.add(k, j), Nat.mul(x, y)), C.shift(k, C.shift(j, Nat.mul(x, y))), WW.shift_comp(k, j, Nat.mul(x, y)))))