def add_succ

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

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

import Base

192def add_succ(+a: Nat, +n: Nat) -> {Nat.add(a, 1n+n) == 1n+Nat.add(a, n) : Nat}:
193  match a:
194    case 0n:
195      {==}
196    case 1n+p:
197      Equal.cong(Nat, Nat, k => 1n+k, Nat.add(p, 1n+n), 1n+Nat.add(p, n), add_succ(p, n))

Uses (3)

Used by (1)

bend-osdev-bpf@0.1.0.0/PROOF:g_count