def ud.add_cancel

bend-osdev-u32@0.1.0.0 · PROOF_div.bend:28

import Base
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL

28# a + r == b + r gives a == b
29def ud.add_cancel(+r: Nat, +a: Nat, +b: Nat, e: {Nat.add(a, r) == Nat.add(b, r) : Nat}) -> {a == b : Nat}:
30  match r:
31    case 0n:
32      Equal.trans(Nat, a, Nat.add(b, 0n), b, Equal.trans(Nat, a, Nat.add(a, 0n), Nat.add(b, 0n), Equal.sym(Nat, Nat.add(a, 0n), a, UL.nat_add_zero(a)), e), UL.nat_add_zero(b))
33    case 1n+q:
34      ud.add_cancel(q, a, b, ud.succ_inj(Nat.add(a, q), Nat.add(b, q), Equal.trans(Nat, 1n+Nat.add(a, q), Nat.add(a, 1n+q), 1n+Nat.add(b, q), Equal.sym(Nat, Nat.add(a, 1n+q), 1n+Nat.add(a, q), UL.nat_add_succ(a, q)), Equal.trans(Nat, Nat.add(a, 1n+q), Nat.add(b, 1n+q), 1n+Nat.add(b, q), e, UL.nat_add_succ(b, q)))))