BendMlNatLemmas.add_swap: def of bend-ml-nat-lemmas@0.1.2.0
Import: import bend-ml-nat-lemmas@0.1.2.0/main.bend as BendMlNatLemmas
Lines 98-107 of bend-ml-nat-lemmas@0.1.2.0/main.bend: https://jend.leeeet.dev/read.txt?path=bend-ml-nat-lemmas@0.1.2.0/main.bend&start_line=98&end_line=107

import Base

# x + (y + z) == y + (x + z): swaps the middle terms of a triple sum.
# (Auxiliary lemma; not a published law.)
def add_swap(x: Nat, +y: Nat, +z: Nat) -> {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}:
  match x:
    case 0n:
      {==}
    case 1n+q:
      %add_succ(y, Nat.add(q, z)) : {1n+Nat.add(q, Nat.add(y, z)) == _ : Nat}
      %add_swap(q, y, z) : {1n+Nat.add(q, Nat.add(y, z)) == 1n+_ : Nat}
      {==}

Uses (3):
  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-ml-nat-lemmas@0.1.2.0/main.bend&name=add_succ