Step.swap3: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend as Step
Lines 123-130 of bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/random/pcg/step.bend&start_line=123&end_line=130

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA

# (L + x) + (y + z) == L + ((y + x) + z)
def swap3(+L: Nat, +x: Nat, +y: Nat, +z: Nat) -> {Nat.add(Nat.add(L, x), Nat.add(y, z)) == Nat.add(L, Nat.add(Nat.add(y, x), z)) : Nat}:
  Equal.trans(Nat, Nat.add(Nat.add(L, x), Nat.add(y, z)), Nat.add(L, Nat.add(x, Nat.add(y, z))), Nat.add(L, Nat.add(Nat.add(y, x), z)),
    NA.add_assoc(L, x, Nat.add(y, z)),
    Equal.cong(Nat, Nat, t => Nat.add(L, t), Nat.add(x, Nat.add(y, z)), Nat.add(Nat.add(y, x), z),
      Equal.trans(Nat, Nat.add(x, Nat.add(y, z)), Nat.add(Nat.add(x, y), z), Nat.add(Nat.add(y, x), z),
        Equal.sym(Nat, Nat.add(Nat.add(x, y), z), Nat.add(x, Nat.add(y, z)), NA.add_assoc(x, y, z)),
        Equal.cong(Nat, Nat, t => Nat.add(t, z), Nat.add(x, y), Nat.add(y, x), NA.add_comm(x, y)))))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm