BT000U

add_right_cancel

Stable checked-use theorem · independently kernel verified

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

A common right addend can be cancelled.

Direct prerequisites: none. The authored body proceeds by structural induction (1), equality transport (4).

Proof neighborhood

Direct dependencies

none

Direct dependents

BT000V add_left_cancel BT0022 mul_left_cancel_nonzero BT002G factor_difference

Formal native tactic body

Dependencies are hypotheses of the historical Alpha-v12 body receipt. The complete historical Alpha-v18 proof bundle independently checks every dependency; current Alpha v25 preserves that checked theorem use without changing Stable membership.

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