def na.sub_zero

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:1677

import Base

1677def na.sub_zero(a: Nat) -> {Nat.sub(a, 0n) == a : Nat}:
1678  match a:
1679    case 0n:
1680      {==}
1681    case 1n+p:
1682      {==}