def un.add_zero

bend-osdev-u32@0.1.0.0 · PROOF.bend:62

import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF

import Base

62def un.add_zero(x: Nat) -> {Nat.add(x, 0n) == x : Nat}:
63  match x:
64    case 0n:
65      {==}
66    case 1n+p:
67      un.succ_cong(Nat.add(p, 0n), p, un.add_zero(p))

Uses (3)

Used by (10)