Mulw.cbn_pow: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as Mulw
Lines 36-45 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend&start_line=36&end_line=45

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
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/poly.bend as PL

def cbn_pow(+j: Nat, +k: Nat) -> {PL.cbn(WD.sc(j, 1n), k) == WD.sc(j, k) : Nat}:
  match j:
    case 0n:
      N.add_zero(k)
    case 1n+ +q:
      +n = WD.sc(q, 1n)
      +e1 = Equal.cong(Nat, Nat, t => PL.cbn(t, k), Nat.double(n), Nat.add(n, n), NA.double_self(n))
      +e2 = cbn_add(n, n, k)
      +e3 = M.cong_add(PL.cbn(n, k), WD.sc(q, k), PL.cbn(n, k), WD.sc(q, k), cbn_pow(q, k), cbn_pow(q, k))
      Equal.trans(Nat, PL.cbn(Nat.double(n), k), Nat.add(PL.cbn(n, k), PL.cbn(n, k)), WD.sc(1n+q, k), Equal.trans(Nat, PL.cbn(Nat.double(n), k), PL.cbn(Nat.add(n, n), k), Nat.add(PL.cbn(n, k), PL.cbn(n, k)), e1, e2), Equal.trans(Nat, Nat.add(PL.cbn(n, k), PL.cbn(n, k)), Nat.add(WD.sc(q, k), WD.sc(q, k)), WD.sc(1n+q, k), e3, M.sc_dbl(q, k)))

Uses (12):
  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.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/crypto/curve25519/mulw.bend&name=cbn_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_add
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=sc_dbl
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=cbn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=double_self
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc