def wn.sub0

bend-osdev-word64@0.1.1.0 · PROOF_mul.bend:40

import Base

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