Num.sc_add: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as Num
Lines 37-45 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&start_line=37&end_line=45

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

# 2^k x + 2^k y == 2^k (x + y)
def sc_add(+k: Nat, +x: Nat, +y: Nat) -> {Nat.add(WD.sc(k, x), WD.sc(k, y)) == WD.sc(k, Nat.add(x, y)) : Nat}:
  match k:
    case 0n:
      {==}
    case 1n+q:
      +e = sc_add(q, x, y)
      +d = Equal.sym(Nat, Nat.double(Nat.add(WD.sc(q, x), WD.sc(q, y))), Nat.add(Nat.double(WD.sc(q, x)), Nat.double(WD.sc(q, y))), NA.double_add(WD.sc(q, x), WD.sc(q, y)))
      Equal.trans(Nat, Nat.add(Nat.double(WD.sc(q, x)), Nat.double(WD.sc(q, y))), Nat.double(Nat.add(WD.sc(q, x), WD.sc(q, y))), Nat.double(WD.sc(q, Nat.add(x, y))), d, Equal.cong(Nat, Nat, t => Nat.double(t), Nat.add(WD.sc(q, x), WD.sc(q, y)), WD.sc(q, Nat.add(x, y)), e))

Uses (8):
  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=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.double
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc