BT000G

no_succ_add_fixed

Stable checked-use theorem · independently kernel verified

Adding a positive successor cannot leave a natural number fixed.

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 p n. S p + n = n -> false

Structural proof guide

Adding a positive successor cannot leave a natural number fixed.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT000H drop_add_prefix_from_fixed BT001B lt_irrefl_expanded

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

11 script commands · 2 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–1

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

  1. L1
    intro p
02Induction on nL2–11

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

  1. L2
    induction n
  2. L3
    intro h
  3. L4
    apply PA1
  4. L5
    rewrite PA3 at h
  5. L6
    exact h
  6. L7
    intro h
  7. L8
    apply IH
  8. L9
    apply PA2
  9. L10
    rewrite PA4 at h
  10. L11
    exact h

Library-wide reading audit

Original exact command ledger · 11 lines
  1. 0001intro p
  2. 0002induction n
  3. 0003intro h
  4. 0004apply PA1
  5. 0005rewrite PA3 at h
  6. 0006exact h
  7. 0007intro h
  8. 0008apply IH
  9. 0009apply PA2
  10. 0010rewrite PA4 at h
  11. 0011exact h