Adc.swap5: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend as Adc
Lines 42-46 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/adc.bend&start_line=42&end_line=46

import Base
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

# (a + A') + (b + B') + c == (a + b + c) + (A' + B') rearranged
def swap5(+a: Nat, +b: Nat, +c: Nat, +X: Nat, +Y: Nat) -> {Nat.add(Nat.add(Nat.add(a, X), Nat.add(b, Y)), c) == Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)) : Nat}:
  +e1 = M.cong_l(Nat.add(Nat.add(a, X), Nat.add(b, Y)), Nat.add(Nat.add(a, b), Nat.add(X, Y)), c, M.add4(a, X, b, Y))
  +e2 = Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, b), Nat.add(X, Y)), c), Nat.add(Nat.add(a, b), Nat.add(Nat.add(X, Y), c)), Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), NA.add_assoc(Nat.add(a, b), Nat.add(X, Y), c), Equal.trans(Nat, Nat.add(Nat.add(a, b), Nat.add(Nat.add(X, Y), c)), Nat.add(Nat.add(a, b), Nat.add(c, Nat.add(X, Y))), Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), M.cong_r(Nat.add(a, b), Nat.add(Nat.add(X, Y), c), Nat.add(c, Nat.add(X, Y)), NA.add_comm(Nat.add(X, Y), c)), Equal.sym(Nat, Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), Nat.add(Nat.add(a, b), Nat.add(c, Nat.add(X, Y))), NA.add_assoc(Nat.add(a, b), c, Nat.add(X, Y)))))
  Equal.trans(Nat, Nat.add(Nat.add(Nat.add(a, X), Nat.add(b, Y)), c), Nat.add(Nat.add(Nat.add(a, b), Nat.add(X, Y)), c), Nat.add(Nat.add(Nat.add(a, b), c), Nat.add(X, Y)), e1, e2)

Uses (9):
  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=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/curve25519/num.bend&name=add4
  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