def pk.sub_zero

bend-osdev-pkcs7@0.1.0.0 · PROOF.bend:41

import Base

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