def add_cancel_r

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/fixgen.bend:63

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

63def add_cancel_r(+a: Nat, +b: Nat, +c: Nat, +e: {Nat.add(a, c) == Nat.add(b, c) : Nat}) -> {a == b : Nat}:
64  +e1 = Equal.trans(Nat, Nat.add(c, a), Nat.add(a, c), Nat.add(b, c), N.add_comm(c, a), e)
65  +e2 = Equal.trans(Nat, Nat.add(c, a), Nat.add(b, c), Nat.add(c, b), e1, N.add_comm(b, c))
66  +e3 = Equal.cong(Nat, Nat, t => Nat.sub(t, c), Nat.add(c, a), Nat.add(c, b), e2)
67  Equal.trans(Nat, a, Nat.sub(Nat.add(c, a), c), b, Equal.sym(Nat, Nat.sub(Nat.add(c, a), c), a, N.add_sub_cancel(c, a)), Equal.trans(Nat, Nat.sub(Nat.add(c, a), c), Nat.sub(Nat.add(c, b), c), b, e3, N.add_sub_cancel(c, b)))