def nat_add_zero

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

import Base

75def nat_add_zero(x: Nat) -> {x == Nat.add(x, 0n) : Nat}:
76  match x:
77    case 0n:
78      {==}
79    case 1n+p:
80      %nat_add_zero(p) : {1n+p == 1n+_ : Nat}
81      {==}