def un.add_cancel_r

bend-osdev-u32@0.1.0.0 · PROOF.bend:105

import Base

105# x + k = y + k: x = y
106def un.add_cancel_r(+x: Nat, +y: Nat, k: Nat, e: {Nat.add(x, k) == Nat.add(y, k) : Nat}) -> {x == y : Nat}:
107  match k:
108    case 0n:
109      Equal.trans(Nat, x, Nat.add(x, 0n), y, Equal.sym(Nat, Nat.add(x, 0n), x, un.add_zero(x)), Equal.trans(Nat, Nat.add(x, 0n), Nat.add(y, 0n), y, e, un.add_zero(y)))
110    case 1n+q:
111      un.add_cancel_r(x, y, q, un.succ_inj(Nat.add(x, q), Nat.add(y, q), Equal.trans(Nat, 1n+Nat.add(x, q), Nat.add(x, 1n+q), 1n+Nat.add(y, q), Equal.sym(Nat, Nat.add(x, 1n+q), 1n+Nat.add(x, q), un.add_succ(x, q)), Equal.trans(Nat, Nat.add(x, 1n+q), Nat.add(y, 1n+q), 1n+Nat.add(y, q), e, un.add_succ(y, q)))))