BT00XC · Bertrand theorem

add_lt_cancel_left

Alpha v34 checked-use theorem · independently kernel and Lean verified; not Stable

A common left summand cancels from strict witness order.

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

∀ c. ∀ a. ∀ b. Lt(c + a,c + b) → Lt(a,b)

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

PD0002 Lt

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall c a b. (exists bcf_lt_gap_b5altcl_source. bcf_lt_gap_b5altcl_source + S (c + a) = c + b) -> (exists bcf_lt_gap_b5altcl_result. bcf_lt_gap_b5altcl_result + S (a) = b)

Proof neighborhood

Direct theorem prerequisites

BT0003 add_assoc BT0002 add_comm BT000V add_left_cancel

Direct theorem dependents

BT00XG division_double_quotient_bit BT00Y8 division_quotient_one_of_bounds BT00Y9 division_quotient_two_of_bounds BT00YB division_first_two_of_two_three_range

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

30 script commands · 16 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)
add assocadd commadd left cancel
01Fix variables and assumptionsL1–4

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

  1. L1
    intro c
  2. L2
    intro a
  3. L3
    intro b
  4. L4
    intro hsource
02Separate the logical casesL5–5

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

  1. L5
    cases hsource
03Construct an explicit witnessL6–6

Supply the displayed value, then prove that it has the required property.

  1. L6
    exists x
04Use earlier factsL7–10

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

  1. L7
    specialize add_left_cancel c
  2. L8
    specialize add_left_cancel (x + S a)
  3. L9
    specialize add_left_cancel b
  4. L10
    apply add_left_cancel
05Calculate and transport equalitiesL11–14

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

  1. L11
    trans x + S (c + a)
  2. L12
    trans c + S (x + a)
  3. L13
    congr
  4. L14
    refl
06Use earlier factsL15–15

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

  1. L15
    apply PA4
07Calculate and transport equalitiesL16–16

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

  1. L16
    trans S (c + (x + a))
08Use earlier factsL17–17

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

  1. L17
    apply PA4
09Calculate and transport equalitiesL18–21

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

  1. L18
    trans S (x + (c + a))
  2. L19
    congr
  3. L20
    trans (c + x) + a
  4. L21
    symm
10Use earlier factsL22–22

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

  1. L22
    apply add_assoc
11Calculate and transport equalitiesL23–24

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

  1. L23
    trans (x + c) + a
  2. L24
    congr
12Use earlier factsL25–25

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

  1. L25
    apply add_comm
13Calculate and transport equalitiesL26–26

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

  1. L26
    refl
14Use earlier factsL27–27

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

  1. L27
    apply add_assoc
15Calculate and transport equalitiesL28–28

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

  1. L28
    symm
16Use earlier factsL29–30

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

  1. L29
    apply PA4
  2. L30
    exact hsource_witness

Library-wide reading audit

Original defined command ledger · 30 lines
  1. 0001intro c
  2. 0002intro a
  3. 0003intro b
  4. 0004intro hsource
  5. 0005cases hsource
  6. 0006exists x
  7. 0007specialize add_left_cancel c
  8. 0008specialize add_left_cancel (x + S a)
  9. 0009specialize add_left_cancel b
  10. 0010apply add_left_cancel
  11. 0011trans x + S (c + a)
  12. 0012trans c + S (x + a)
  13. 0013congr
  14. 0014refl
  15. 0015apply PA4
  16. 0016trans S (c + (x + a))
  17. 0017apply PA4
  18. 0018trans S (x + (c + a))
  19. 0019congr
  20. 0020trans (c + x) + a
  21. 0021symm
  22. 0022apply add_assoc
  23. 0023trans (x + c) + a
  24. 0024congr
  25. 0025apply add_comm
  26. 0026refl
  27. 0027apply add_assoc
  28. 0028symm
  29. 0029apply PA4
  30. 0030exact hsource_witness