def wn.sub0

bend-osdev-word64@0.1.1.0 · PROOF_text.bend:42

import Base

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