def mul_sc_l

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64mul.bend:113

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-math@1.0.0.0/proofs/lib/arith.bend as AR

113# 2^k q * d == 2^k (q d)
114def mul_sc_l(+k: Nat, +q: Nat, +d: Nat) -> {Nat.mul(WD.sc(k, q), d) == WD.sc(k, Nat.mul(q, d)) : Nat}:
115  Equal.sym(Nat, WD.sc(k, Nat.mul(q, d)), Nat.mul(WD.sc(k, q), d), AR.sc_mul(k, q, d))