def sub0

bendtorch@1.3.0.0 · PROOF.bend:185

import Base

185# n - 0 is n
186def sub0(+n: Nat) -> {Nat.sub(n, 0n) == n : Nat}:
187  match n:
188    case 0n:
189      {==}
190    case 1n+p:
191      {==}