def swap_ends

bend-collections-laws-math@1.0.0.0 · proofs/math/random/shuffle.bend:40

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N

40# (a + c) + b == (b + c) + a
41def swap_ends(+a: Nat, +b: Nat, +c: Nat) -> {Nat.add(Nat.add(a, c), b) == Nat.add(Nat.add(b, c), a) : Nat}:
42  Equal.trans(Nat, Nat.add(Nat.add(a, c), b), Nat.add(a, Nat.add(c, b)), Nat.add(Nat.add(b, c), a),
43    N.add_assoc(a, c, b),
44    Equal.trans(Nat, Nat.add(a, Nat.add(c, b)), Nat.add(a, Nat.add(b, c)), Nat.add(Nat.add(b, c), a),
45      Equal.cong(Nat, Nat, t => Nat.add(a, t), Nat.add(c, b), Nat.add(b, c), N.add_comm(c, b)),
46      N.add_comm(a, Nat.add(b, c))))