def ud.sub_zero

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:11

import Base

11def ud.sub_zero(a: Nat) -> {Nat.sub(a, 0n) == a : Nat}:
12  match a:
13    case 0n:
14      {==}
15    case 1n+p:
16      {==}