BT000H

drop_add_prefix_from_fixed

Stable checked-use theorem · independently kernel verified

A fixed-point equation remains fixed after dropping an additive prefix.

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 n. (b + a) + n = n -> a + n = n

Structural proof guide

A fixed-point equation remains fixed after dropping an additive prefix.

Direct prerequisites: zero_add, add_succ_left, no_succ_add_fixed. The authored body proceeds by structural induction (1), equality transport (2).

Proof neighborhood

Direct dependencies

BT0000 zero_add BT0001 add_succ_left BT000G no_succ_add_fixed

Direct dependents

BT000I antisymm_from_witnesses

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

17 script commands · 6 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.

Named ingredients (3)
zero addadd succ leftno succ add fixed
01Fix variables and assumptionsL1–1

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

  1. L1
    intro a
02Induction on bL2–9

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

  1. L2
    induction b
  2. L3
    intro n
  3. L4
    intro h
  4. L5
    specialize zero_add a
  5. L6
    rewrite zero_add at h
  6. L7
    exact h
  7. L8
    intro n
  8. L9
    intro h
03Separate the logical casesL10–10

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L10
    exfalso
04Use earlier factsL11–15

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

  1. L11
    specialize no_succ_add_fixed (b + a)
  2. L12
    specialize no_succ_add_fixed n
  3. L13
    apply no_succ_add_fixed
  4. L14
    specialize add_succ_left b
  5. L15
    specialize add_succ_left a
05Calculate and transport equalitiesL16–16

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L16
    rewrite add_succ_left at h
06Use earlier factsL17–17

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

  1. L17
    exact h

Library-wide reading audit

Original exact command ledger · 17 lines
  1. 0001intro a
  2. 0002induction b
  3. 0003intro n
  4. 0004intro h
  5. 0005specialize zero_add a
  6. 0006rewrite zero_add at h
  7. 0007exact h
  8. 0008intro n
  9. 0009intro h
  10. 0010exfalso
  11. 0011specialize no_succ_add_fixed (b + a)
  12. 0012specialize no_succ_add_fixed n
  13. 0013apply no_succ_add_fixed
  14. 0014specialize add_succ_left b
  15. 0015specialize add_succ_left a
  16. 0016rewrite add_succ_left at h
  17. 0017exact h