def nat.add_zero

bend-osdev-algo@0.1.0.0 · PROOF.bend:107

import Base

107def nat.add_zero(a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
108  match a:
109    case 0n:
110      {==}
111    case 1n+p:
112      %nat.add_zero(p) : {1n+Nat.add(p, 0n) == 1n+_ : Nat}
113      {==}