PROOF.un.add_swap: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 665-671 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=665&end_line=671

import Base

# (s + b) + k = (s + k) + b
def un.add_swap(s: Nat, +b: Nat, +k: Nat) -> {Nat.add(Nat.add(s, b), k) == Nat.add(Nat.add(s, k), b) : Nat}:
  match s:
    case 0n:
      un.add_comm(b, k)
    case 1n+p:
      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):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_comm
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.succ_cong