Poly.take_drop_val: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as Poly
Lines 323-337 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&start_line=323&end_line=337

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/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 take_drop_val(+n: Nat, +xs: List<&2, U32>) -> {FS.value(xs) == Nat.add(FS.value(F.take(n, xs)), LM.sh(F.take(n, xs), FS.value(F.drop(n, xs)))) : Nat}:
  match n xs:
    case 0n _:
      {==}
    case 1n+m Nil{}:
      {==}
    case 1n+ +m Con{+x, +xt}:
      +T = FS.value(F.take(m, xt))
      +D = LM.sh(F.take(m, xt), FS.value(F.drop(m, xt)))
      +ih = take_drop_val(m, xt)
      +e1 = M.cong_r(v(x), C.shift(8n, FS.value(xt)), C.shift(8n, Nat.add(T, D)), M.cong_sc(8n, FS.value(xt), Nat.add(T, D), ih))
      +e2 = M.cong_r(v(x), C.shift(8n, Nat.add(T, D)), Nat.add(C.shift(8n, T), C.shift(8n, D)), Equal.sym(Nat, Nat.add(C.shift(8n, T), C.shift(8n, D)), C.shift(8n, Nat.add(T, D)), M.sc_add(8n, T, D)))
      +e3 = Equal.sym(Nat, Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), Nat.add(v(x), Nat.add(C.shift(8n, T), C.shift(8n, D))), NA.add_assoc(v(x), C.shift(8n, T), C.shift(8n, D)))
      Equal.trans(Nat, Nat.add(v(x), C.shift(8n, FS.value(xt))), Nat.add(v(x), C.shift(8n, Nat.add(T, D))), Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), e1,
        Equal.trans(Nat, Nat.add(v(x), C.shift(8n, Nat.add(T, D))), Nat.add(v(x), Nat.add(C.shift(8n, T), C.shift(8n, D))), Nat.add(Nat.add(v(x), C.shift(8n, T)), C.shift(8n, D)), e2, e3))

Uses (16):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=sh
  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/crypto/curve25519/num.bend&name=cong_sc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=v
  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/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=drop
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=take