PROOF.un.add_cancel_r: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 105-111 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=105&end_line=111

import Base

# x + k = y + k: x = y
def un.add_cancel_r(+x: Nat, +y: Nat, k: Nat, e: {Nat.add(x, k) == Nat.add(y, k) : Nat}) -> {x == y : Nat}:
  match k:
    case 0n:
      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)))
    case 1n+q:
      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)))))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_succ
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.add_zero
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.succ_inj