def shift_mul_r

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

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

397def shift_mul_r(+k: Nat, +x: Nat, +y: Nat) -> {Nat.mul(x, C.shift(k, y)) == C.shift(k, Nat.mul(x, y)) : Nat}:
398  Equal.trans(Nat, Nat.mul(x, C.shift(k, y)), Nat.mul(C.shift(k, y), x), C.shift(k, Nat.mul(x, y)), NA.mul_comm(x, C.shift(k, y)), Equal.trans(Nat, Nat.mul(C.shift(k, y), x), C.shift(k, Nat.mul(y, x)), C.shift(k, Nat.mul(x, y)), shift_mul_l(k, y, x), Equal.cong(Nat, Nat, t => C.shift(k, t), Nat.mul(y, x), Nat.mul(x, y), NA.mul_comm(y, x))))