Lemma·L10
Cancellation for addition
Equal sums with an equal summand force the other summands equal.
for all
, with
from D027.
In words
If adding k to m and to n on the left gives equal results then m and n are equal, and if adding k on the right gives equal results then m and n are equal, for all natural numbers k, m, n.
Never needed: F05 · F10 · F11 · F12 · F13 · A02 · A03 · A04 · A05 · A07 (computed from the citation graph, not asserted).
Proof
- 1Left form, by induction on (T05, Separation). Base: if then , since and by Claim A of L09.
- 2Step: assume the implication holds for , and let . By Claim B of L09, . The successor is injective by Peano (P4), so , and the induction hypothesis gives .
- 3Right form: if , rewrite both sides with commutativity to and apply the left form (substitutivity).
∎
Remarks
Cancellation is the ghost of subtraction:
has no additive inverses, but equal sums can still be stripped of a common summand. It is used constantly, from the division algorithm to the counting arguments in L26. Note where injectivity of the successor enters: cancellation for
is Peano (P4) amplified by induction.