def shift_mul

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

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

361def shift_mul(+k: Nat, +x: Nat) -> {C.shift(k, x) == Nat.mul(x, C.shift(k, 1n)) : Nat}:
362  match k:
363    case 0n:
364      Equal.sym(Nat, Nat.mul(x, 1n), x, NA.mul_one(x))
365    case 1n+ +p:
366      Equal.trans(Nat, Nat.double(C.shift(p, x)), Nat.double(Nat.mul(x, C.shift(p, 1n))), Nat.mul(x, Nat.double(C.shift(p, 1n))), Equal.cong(Nat, Nat, t => Nat.double(t), C.shift(p, x), Nat.mul(x, C.shift(p, 1n)), shift_mul(p, x)), dbl_mul(x, C.shift(p, 1n)))