Canon.iz_sum: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as Canon
Lines 148-156 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&start_line=148&end_line=156

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/spec/crypto/curve25519/field.bend as FS

def iz_sum(+xs: List<&2, U32>) -> {Nat.is_eq(sumv(xs), 0n) == Nat.is_eq(FS.value(xs), 0n) : Bool}:
  match xs:
    case Nil{}:
      {==}
    case Con{+y, +yt}:
      +e1 = iz_add(v(y), sumv(yt))
      +e2 = iz_add(v(y), C.shift(8n, FS.value(yt)))
      +e3 = Equal.trans(Bool, Nat.is_eq(C.shift(8n, FS.value(yt)), 0n), Nat.is_eq(FS.value(yt), 0n), Nat.is_eq(sumv(yt), 0n), iz_sc(8n, FS.value(yt)), Equal.sym(Bool, Nat.is_eq(sumv(yt), 0n), Nat.is_eq(FS.value(yt), 0n), iz_sum(yt)))
      Equal.trans(Bool, Nat.is_eq(Nat.add(v(y), sumv(yt)), 0n), Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(sumv(yt), 0n)), Nat.is_eq(Nat.add(v(y), C.shift(8n, FS.value(yt))), 0n), e1, Equal.trans(Bool, Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(sumv(yt), 0n)), Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(C.shift(8n, FS.value(yt)), 0n)), Nat.is_eq(Nat.add(v(y), C.shift(8n, FS.value(yt))), 0n), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_eq(v(y), 0n), z), Nat.is_eq(sumv(yt), 0n), Nat.is_eq(C.shift(8n, FS.value(yt)), 0n), Equal.sym(Bool, Nat.is_eq(C.shift(8n, FS.value(yt)), 0n), Nat.is_eq(sumv(yt), 0n), e3)), Equal.sym(Bool, Nat.is_eq(Nat.add(v(y), C.shift(8n, FS.value(yt))), 0n), Bool.and(Nat.is_eq(v(y), 0n), Nat.is_eq(C.shift(8n, FS.value(yt)), 0n)), e2)))

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  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.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=iz_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=iz_sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=sumv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend&name=shift