Cong.pow_one_base: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as Cong
Lines 65-72 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend&start_line=65&end_line=72

import Base

def pow_one_base(+k: Nat) -> {Nat.pow(1n, k) == 1n : Nat}:
  match k:
    case 0n:
      {==}
    case 1n+ +q:
      +e = pow_one_base(q)
      %Equal.sym(Nat, Nat.pow(1n, q), 1n, e) : {Nat.mul(1n, _) == 1n : Nat}
      {==}

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.pow