def add_swap

bend-ml-nat-lemmas@0.1.2.0 · main.bend:98

import Base

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