def sub_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/nat.bend:283

import Base

283def sub_zero(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
284  match n:
285    case 0n:
286      {==}
287    case 1n+p:
288      {==}