~/jendhub

def un.add_swap

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

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

665# (s + b) + k = (s + k) + b
666def un.add_swap(s: Nat, +b: Nat, +k: Nat) -> {Nat.add(Nat.add(s, b), k) == Nat.add(Nat.add(s, k), b) : Nat}:
667  match s:
668    case 0n:
669      un.add_comm(b, k)
670    case 1n+p:
671      un.succ_cong(Nat.add(Nat.add(p, b), k), Nat.add(Nat.add(p, k), b), un.add_swap(p, b, k))

Uses (4)

Used by (1)