Registry · Proposition I.P17 established formalized

I.P17 — Universal Additive Cancellation

n + a = n + b implies a = b. Additive cancellation is UNIVERSAL: no positivity guard needed. Follows from rho-injectivity.

Book I Part 3 Ch. 15

Dependency Graph

Depends on (2)

I.D10 I.P02

Depended on by (1)

I.T17

Lean Formalization

Module: TauLib.BookI.Denotation.Structural

Symbol: Tau.Denotation.tauIdx_add_left_cancel