def wn.sub0

bend-osdev-word64@0.1.1.0 · PROOF_div.bend:44

import Base

44def wn.sub0(x: Nat) -> {Nat.sub(x, 0n) == x : Nat}:
45  match x:
46    case 0n:
47      {==}
48    case 1n+ +p:
49      {==}