def zero_sub

bend-collections-laws-math@1.0.0.0 · proofs/lib/two_list.bend:10

import Base

10def zero_sub(+k: Nat) -> {Nat.sub(0n, k) == 0n : Nat}:
11  match k:
12    case 0n:
13      {==}
14    case 1n+p:
15      {==}