def mul_sc_r

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

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
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

109# q * 2^k d == 2^k (q d)
110def mul_sc_r(+k: Nat, +q: Nat, +d: Nat) -> {Nat.mul(q, WD.sc(k, d)) == WD.sc(k, Nat.mul(q, d)) : Nat}:
111  Equal.trans(Nat, Nat.mul(q, WD.sc(k, d)), Nat.mul(WD.sc(k, d), q), WD.sc(k, Nat.mul(q, d)), NA.mul_comm(q, WD.sc(k, d)), Equal.trans(Nat, Nat.mul(WD.sc(k, d), q), WD.sc(k, Nat.mul(d, q)), WD.sc(k, Nat.mul(q, d)), Equal.sym(Nat, WD.sc(k, Nat.mul(d, q)), Nat.mul(WD.sc(k, d), q), AR.sc_mul(k, d, q)), cong_sc(k, Nat.mul(d, q), Nat.mul(q, d), NA.mul_comm(d, q))))