def na.add_zero

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

import Base

1661def na.add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
1662  match a:
1663    case 0n:
1664      {==}
1665    case 1n+p:
1666      %na.add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
1667      {==}