def nat_sub_zero

bend-osdev-aead@0.1.0.0 · PROOF.bend:91

import Base

91def nat_sub_zero(x: Nat) -> {x == Nat.sub(x, 0n) : Nat}:
92  match x:
93    case 0n:
94      {==}
95    case 1n+p:
96      {==}