def zsub

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/argon2/memory.bend:40

import Base

40def zsub(+n: Nat) -> {Nat.sub(0n, n) == 0n : Nat}:
41  match n:
42    case 0n:
43      {==}
44    case 1n+p:
45      {==}