Limbs.add_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 54-74 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=54&end_line=74

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 add_v(xs: List<&2, Nat>, ys: List<&2, Nat>) -> {ev(L.add(xs, ys)) == Nat.add(ev(xs), ev(ys)) : Nat}:
  match xs ys:
    case Nil{} Nil{}:
      {==}
    case Nil{} y <> yt:
      {==}
    case +x <> +xt Nil{}:
      Equal.sym(Nat, Nat.add(ev(x <> xt), 0n), ev(x <> xt), NA.add_zero(ev(x <> xt)))
    case +x <> +xt +y <> +yt:
      %Equal.sym(Nat, ev(L.add(xt, yt)), Nat.add(ev(xt), ev(yt)), add_v(xt, yt)) : {Nat.add(Nat.add(x, y), C.shift(16n, _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
      %Equal.sym(Nat, C.shift(16n, Nat.add(ev(xt), ev(yt))), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))), WW.shift_add(16n, ev(xt), ev(yt))) : {Nat.add(Nat.add(x, y), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.add(x, y), Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(x, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))), NA.add_assoc(x, y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt))))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
      %Equal.sym(Nat, Nat.add(y, Nat.add(C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))), Nat.add(C.shift(16n, ev(xt)), Nat.add(y, C.shift(16n, ev(yt)))), NA.add_swap(y, C.shift(16n, ev(xt)), C.shift(16n, ev(yt)))) : {Nat.add(x, _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : 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(x, Nat.add(C.shift(16n, ev(xt)), _)) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_swap(x, C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), y))) : {_ == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : Nat}
      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), _) == Nat.add(Nat.add(x, C.shift(16n, ev(xt))), Nat.add(y, C.shift(16n, ev(yt)))) : 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, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(_, Nat.add(y, C.shift(16n, ev(yt)))) : 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, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(Nat.add(C.shift(16n, ev(xt)), x), _) : Nat}
      %Equal.sym(Nat, Nat.add(Nat.add(C.shift(16n, ev(xt)), x), Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(xt)), Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y))), NA.add_assoc(C.shift(16n, ev(xt)), x, Nat.add(C.shift(16n, ev(yt)), y))) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == _ : Nat}
      %Equal.sym(Nat, Nat.add(x, Nat.add(C.shift(16n, ev(yt)), y)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y)), NA.add_swap(x, C.shift(16n, ev(yt)), y)) : {Nat.add(C.shift(16n, ev(xt)), Nat.add(C.shift(16n, ev(yt)), Nat.add(x, y))) == Nat.add(C.shift(16n, ev(xt)), _) : 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=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_assoc
  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=add_swap
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend&name=shift_add
  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