PA0012

add_right_cancel

Stable checked-use theorem · independently closed

A common right addend can be cancelled.

Current library: Alpha v34, 4,223 checked-use theorems; Stable remains 432. Historical first admissions, original proof editions, and non-admitted aliases are preserved. Exact original first-admission records.

Exact expanded PA statement

forall a b c. a + c = b + c -> a = b

Structural proof guide

Generated structural guide

A common right addend can be cancelled.

This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.

The proof proceeds by structural induction (1), equality transport (4).

Referenced ingredients

none

Proof neighborhood

Direct dependencies

none

Direct dependents

PA0013 factor_difference PA002B add_left_cancel PA006S mul_left_cancel_nonzero PA006T odd_half_unique PA006Y odd_upper_remainder_reflection

Formal native tactic body

Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.

Read the argument

Proof checkpoints

13 script commands · 3 reading checkpoints · 0 local claims

This is a reading aid, not a new proof or a proof-tree certificate. Checkpoint groups are consecutive commands, not inferred branch boundaries. Every step links to the preserved script.

01Fix variables and assumptionsL1–2

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro a
  2. L2
    intro b
02Induction on cL3–12

Split the argument into the base and successor obligations. The induction hypothesis is available only in the successor branch.

  1. L3
    induction c
  2. L4
    intro h
  3. L5
    rewrite PA3 at h
  4. L6
    rewrite PA3 at h
  5. L7
    exact h
  6. L8
    intro h
  7. L9
    apply IH
  8. L10
    apply PA2
  9. L11
    rewrite PA4 at h
  10. L12
    rewrite PA4 at h
03Use earlier factsL13–13

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L13
    exact h

Library-wide reading audit

Original exact command ledger · 13 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003induction c
  4. 0004intro h
  5. 0005rewrite PA3 at h
  6. 0006rewrite PA3 at h
  7. 0007exact h
  8. 0008intro h
  9. 0009apply IH
  10. 0010apply PA2
  11. 0011rewrite PA4 at h
  12. 0012rewrite PA4 at h
  13. 0013exact h