BT000H · Bertrand theorem

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.

Statement with defined notation

forall a b n. (b + a) + n = n -> a + n = n

Every purple notation token opens its conservative definition. Expanding the displayed statement recovers the exact first-order Peano-arithmetic formula checked by the unchanged kernel.

Definitions used by this theorem

In the theorem statement

none

0 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b n. (b + a) + n = n -> a + n = n

Proof neighborhood

Direct theorem prerequisites

BT0000 zero_add BT0001 add_succ_left BT000G no_succ_add_fixed

Direct theorem dependents

BT000I antisymm_from_witnesses

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. Every changed line has an exact-AST conservative-expansion receipt; the kernel still receives the immutable original tactic script.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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 defined 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