Limbs.conv_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 92-106 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=92&end_line=106

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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend as SR

def conv_v(xs: List<&2, Nat>, +ys: List<&2, Nat>) -> {ev(L.conv(xs, ys)) == Nat.mul(ev(xs), ev(ys)) : Nat}:
  match xs:
    case Nil{}:
      {==}
    case +x <> +xt:
      %Equal.sym(Nat, ev(L.add(L.scal(x, ys), 0n <> L.conv(xt, ys))), Nat.add(ev(L.scal(x, ys)), ev(0n <> L.conv(xt, ys))), add_v(L.scal(x, ys), 0n <> L.conv(xt, ys))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
      %Equal.sym(Nat, ev(L.scal(x, ys)), Nat.mul(ev(ys), x), scal_v(x, ys)) : {Nat.add(_, ev(0n <> L.conv(xt, ys))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
      %Equal.sym(Nat, ev(L.conv(xt, ys)), Nat.mul(ev(xt), ev(ys)), conv_v(xt, ys)) : {Nat.add(Nat.mul(ev(ys), x), Nat.add(0n, C.shift(16n, _))) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
      %Equal.sym(Nat, Nat.add(0n, C.shift(16n, Nat.mul(ev(xt), ev(ys)))), C.shift(16n, Nat.mul(ev(xt), ev(ys))), SR.zero_add(C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {Nat.add(Nat.mul(ev(ys), x), _) == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys)))), Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)), NA.add_comm(Nat.mul(ev(ys), x), C.shift(16n, Nat.mul(ev(xt), ev(ys))))) : {_ == Nat.mul(Nat.add(x, C.shift(16n, ev(xt))), ev(ys)) : Nat}
      %Equal.sym(Nat, Nat.add(x, C.shift(16n, ev(xt))), Nat.add(C.shift(16n, ev(xt)), x), NA.add_comm(x, C.shift(16n, ev(xt)))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.mul(_, ev(ys)) : Nat}
      %Equal.sym(Nat, Nat.mul(Nat.add(C.shift(16n, ev(xt)), x), ev(ys)), Nat.add(Nat.mul(C.shift(16n, ev(xt)), ev(ys)), Nat.mul(x, ev(ys))), NA.mul_add_right(C.shift(16n, ev(xt)), x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == _ : Nat}
      %Equal.sym(Nat, Nat.mul(C.shift(16n, ev(xt)), ev(ys)), C.shift(16n, Nat.mul(ev(xt), ev(ys))), WW.shift_mul_l(16n, ev(xt), ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(_, Nat.mul(x, ev(ys))) : Nat}
      %Equal.sym(Nat, Nat.mul(x, ev(ys)), Nat.mul(ev(ys), x), NA.mul_comm(x, ev(ys))) : {Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), Nat.mul(ev(ys), x)) == Nat.add(C.shift(16n, Nat.mul(ev(xt), ev(ys))), _) : Nat}
      {==}

Uses (17):
  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=add_v
  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/crypto/secp256k1/limbs.bend&name=scal_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/secp256k1/semiring.bend&name=zero_add
  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=add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=conv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/limbs.bend&name=scal