Fold.add0_val: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as Fold
Lines 73-77 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend&start_line=73&end_line=77

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
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
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/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM

def add0_val(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +xt: List<&2, U32>, +k: U32, +h: {Nat.is_lt(Nat.add(v(x), v(k)), WD.sc(32n, one)) == True{} : Bool}) -> {FS.value(F.add0(Con{x, xt}, k)) == Nat.add(FS.value(Con{x, xt}), v(k)) : Nat}:
  +X = C.shift(8n, FS.value(xt))
  +e1 = M.cong_l(v(U32.add(x, k)), Nat.add(v(x), v(k)), X, LM.add_v(one, h1, x, k, h))
  +e2 = Equal.trans(Nat, Nat.add(Nat.add(v(x), v(k)), X), Nat.add(v(x), Nat.add(v(k), X)), Nat.add(Nat.add(v(x), X), v(k)), NA.add_assoc(v(x), v(k), X), Equal.trans(Nat, Nat.add(v(x), Nat.add(v(k), X)), Nat.add(v(x), Nat.add(X, v(k))), Nat.add(Nat.add(v(x), X), v(k)), M.cong_r(v(x), Nat.add(v(k), X), Nat.add(X, v(k)), NA.add_comm(v(k), X)), Equal.sym(Nat, Nat.add(Nat.add(v(x), X), v(k)), Nat.add(v(x), Nat.add(X, v(k))), NA.add_assoc(v(x), X, v(k)))))
  Equal.trans(Nat, Nat.add(v(U32.add(x, k)), X), Nat.add(Nat.add(v(x), v(k)), X), Nat.add(Nat.add(v(x), X), v(k)), e1, e2)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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
  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_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=add_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_l
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r
  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/word.bend&name=sc
  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
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=add0