~/jendhub

def uq.add_zero

bend-osdev-algo@0.1.0.0 · proof_u32.bend:64

import bend-osdev-algo@0.1.0.0/proof_u32.bend as ProofU32
import Base

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

Uses (3)

Used by (1)