~/jendhub

def tr.add_succ

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:882

import bend-osdev-cipher-modes@0.1.0.0/PROOF.bend as PROOF
import Base

882def tr.add_succ(+a: Nat, +n: Nat) -> {Nat.add(a, 1n+n) == 1n+Nat.add(a, n) : Nat}:
883  match a:
884    case 0n:
885      {==}
886    case 1n+q:
887      Equal.cong(Nat, Nat, x => 1n+x, Nat.add(q, 1n+n), 1n+Nat.add(q, n), tr.add_succ(q, n))

Uses (3)

Used by (1)