Limbs.scal_v: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend as Limbs
Lines 76-90 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&start_line=76&end_line=90

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/src/crypto/secp256k1/limbs.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

def scal_v(+a: Nat, ys: List<&2, Nat>) -> {ev(L.scal(a, ys)) == Nat.mul(ev(ys), a) : Nat}:
  match ys:
    case Nil{}:
      {==}
    case +y <> +yt:
      %Equal.sym(Nat, ev(L.scal(a, yt)), Nat.mul(ev(yt), a), scal_v(a, yt)) : {Nat.add(Nat.mul(y, a), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
      %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(_, C.shift(16n, Nat.mul(ev(yt), a))) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
      %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(Nat.mul(a, y), C.shift(16n, _)) == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt)))), Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)), NA.add_comm(Nat.mul(a, y), C.shift(16n, Nat.mul(a, ev(yt))))) : {_ == Nat.mul(Nat.add(y, C.shift(16n, ev(yt))), a) : Nat}
      %Equal.sym(Nat, Nat.add(y, C.shift(16n, ev(yt))), Nat.add(C.shift(16n, ev(yt)), y), NA.add_comm(y, C.shift(16n, ev(yt)))) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.mul(_, a) : Nat}
      %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(yt)), y), a), Nat.add(Nat.mul(C.shift(16n, ev(yt)), a), Nat.mul(y, a)), NA.mul_add_right(C.shift(16n, ev(yt)), y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == _ : Nat}
      %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(yt)), a), C.shift(16n, Nat.mul(ev(yt), a)), WW.shift_mul_l(16n, ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(_, Nat.mul(y, a)) : Nat}
      %Equal.sym(Nat, Nat.mul(ev(yt), a), Nat.mul(a, ev(yt)), NA.mul_comm(ev(yt), a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, _), Nat.mul(y, a)) : Nat}
      %Equal.sym(Nat, Nat.mul(y, a), Nat.mul(a, y), NA.mul_comm(y, a)) : {Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), Nat.mul(a, y)) == Nat.add(C.shift(16n, Nat.mul(a, ev(yt))), _) : Nat}
      {==}

Uses (12):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/limbs.bend&name=ev
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_add_right
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=mul_comm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_mul_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=scal