def shift

bend-collections-laws-math@1.0.0.0 · proofs/math/natural/inverse.bend:39

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

39# (z + c) + k == M + z when c + k == M
40def shift(+z: Nat, +c: Nat, +k: Nat, +mm: Nat, +e: {Nat.add(c, k) == mm : Nat}) -> {Nat.add(Nat.add(z, c), k) == Nat.add(mm, z) : Nat}:
41  Equal.trans(Nat, Nat.add(Nat.add(z, c), k), Nat.add(z, Nat.add(c, k)), Nat.add(mm, z), A.add_assoc(z, c, k), Equal.trans(Nat, Nat.add(z, Nat.add(c, k)), Nat.add(z, mm), Nat.add(mm, z), Equal.cong(Nat, Nat, w => Nat.add(z, w), Nat.add(c, k), mm, e), A.add_comm(z, mm)))