def assoc3

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

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

48# (h + x) + y == h + (x + y), stated for the step of put_occ
49def assoc3(+h: Nat, +x: Nat, +y: Nat, +z: Nat, +e: {Nat.add(x, y) == z : Nat}) -> {Nat.add(Nat.add(h, x), y) == Nat.add(h, z) : Nat}:
50  Equal.trans(Nat, Nat.add(Nat.add(h, x), y), Nat.add(h, Nat.add(x, y)), Nat.add(h, z), N.add_assoc(h, x, y),
51    Equal.cong(Nat, Nat, t => Nat.add(h, t), Nat.add(x, y), z, e))