~/jendhub

def add_zero

bend-osdev-bpf@0.1.0.0 · PROOF.bend:199

import bend-osdev-bpf@0.1.0.0/PROOF.bend as PROOF
import Base

199def add_zero(+a: Nat) -> {Nat.add(a, 0n) == a : Nat}:
200  match a:
201    case 0n:
202      {==}
203    case 1n+p:
204      Equal.cong(Nat, Nat, k => 1n+k, Nat.add(p, 0n), p, add_zero(p))

Uses (3)

Used by (1)