def shift_mul_l

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/width.bend:393

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

393def shift_mul_l(+k: Nat, +x: Nat, +y: Nat) -> {Nat.mul(C.shift(k, x), y) == C.shift(k, Nat.mul(x, y)) : Nat}:
394  +s1 = C.shift(k, 1n)
395  Equal.trans(Nat, Nat.mul(C.shift(k, x), y), Nat.mul(Nat.mul(x, s1), y), C.shift(k, Nat.mul(x, y)), Equal.cong(Nat, Nat, t => Nat.mul(t, y), C.shift(k, x), Nat.mul(x, s1), shift_mul(k, x)), Equal.trans(Nat, Nat.mul(Nat.mul(x, s1), y), Nat.mul(x, Nat.mul(s1, y)), C.shift(k, Nat.mul(x, y)), NA.mul_assoc(x, s1, y), Equal.trans(Nat, Nat.mul(x, Nat.mul(s1, y)), Nat.mul(x, Nat.mul(y, s1)), C.shift(k, Nat.mul(x, y)), Equal.cong(Nat, Nat, t => Nat.mul(x, t), Nat.mul(s1, y), Nat.mul(y, s1), NA.mul_comm(s1, y)), Equal.trans(Nat, Nat.mul(x, Nat.mul(y, s1)), Nat.mul(Nat.mul(x, y), s1), C.shift(k, Nat.mul(x, y)), Equal.sym(Nat, Nat.mul(Nat.mul(x, y), s1), Nat.mul(x, Nat.mul(y, s1)), NA.mul_assoc(x, y, s1)), Equal.sym(Nat, C.shift(k, Nat.mul(x, y)), Nat.mul(Nat.mul(x, y), s1), shift_mul(k, Nat.mul(x, y)))))))