def pow_one_base

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/cong.bend:65

import Base

65def pow_one_base(+k: Nat) -> {Nat.pow(1n, k) == 1n : Nat}:
66  match k:
67    case 0n:
68      {==}
69    case 1n+ +q:
70      +e = pow_one_base(q)
71      %Equal.sym(Nat, Nat.pow(1n, q), 1n, e) : {Nat.mul(1n, _) == 1n : Nat}
72      {==}