BT0097

lt_three_cases

Stable checked-use theorem · independently kernel verified

Every natural strictly below three is zero, one, or two.

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 x. (exists h. h + S x = 3) -> x = 0 \/ x = 1 \/ x = 2

Structural proof guide

Every natural strictly below three is zero, one, or two.

Direct prerequisites: le_of_succ_le_succ, le_eq_or_lt, le_zero. The authored body proceeds by case analysis (2), intermediate claims (5).

Proof neighborhood

Direct dependencies

BT0017 le_of_succ_le_succ BT001C le_eq_or_lt BT000Y le_zero

Direct dependents

BT010B floor_sqrt_two_le_of_two_lt

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

38 script commands · 12 reading checkpoints · 5 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)
le of succ le succle eq or ltle zero
01Fix variables and assumptionsL1–2

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

  1. L1
    intro x
  2. L2
    intro hb
02Establish hle2L3–7

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L3
    have hle2 : exists h. h + x = 2
  2. L4
    specialize le_of_succ_le_succ x
  3. L5
    specialize le_of_succ_le_succ 2
  4. L6
    apply le_of_succ_le_succ
  5. L7
    exact hb
03Establish hc2L8–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L8
    have hc2 : x = 2 \/ exists h. h + S x = 2
  2. L9
    specialize le_eq_or_lt x
  3. L10
    specialize le_eq_or_lt 2
  4. L11
    apply le_eq_or_lt
  5. L12
    exact hle2
04Separate the logical casesL13–14

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

  1. L13
    cases hc2
  2. L14
    right
05Use earlier factsL15–15

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

  1. L15
    exact hc2_left
06Separate the logical casesL16–16

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

  1. L16
    left
07Establish hle1L17–21

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L17
    have hle1 : exists h. h + x = 1
  2. L18
    specialize le_of_succ_le_succ x
  3. L19
    specialize le_of_succ_le_succ 1
  4. L20
    apply le_of_succ_le_succ
  5. L21
    exact hc2_right
08Establish hc1L22–26

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.

  1. L22
    have hc1 : x = 1 \/ exists h. h + S x = 1
  2. L23
    specialize le_eq_or_lt x
  3. L24
    specialize le_eq_or_lt 1
  4. L25
    apply le_eq_or_lt
  5. L26
    exact hle1
09Separate the logical casesL27–28

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

  1. L27
    cases hc1
  2. L28
    right
10Use earlier factsL29–29

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

  1. L29
    exact hc1_left
11Separate the logical casesL30–30

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

  1. L30
    left
12Establish hle0L31–38

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L31
    have hle0 : exists h. h + x = 0
  2. L32
    specialize le_of_succ_le_succ x
  3. L33
    specialize le_of_succ_le_succ 0
  4. L34
    apply le_of_succ_le_succ
  5. L35
    exact hc1_right
  6. L36
    specialize le_zero x
  7. L37
    apply le_zero
  8. L38
    exact hle0

Library-wide reading audit

Original exact command ledger · 38 lines
  1. 0001intro x
  2. 0002intro hb
  3. 0003have hle2 : exists h. h + x = 2
  4. 0004specialize le_of_succ_le_succ x
  5. 0005specialize le_of_succ_le_succ 2
  6. 0006apply le_of_succ_le_succ
  7. 0007exact hb
  8. 0008have hc2 : x = 2 \/ exists h. h + S x = 2
  9. 0009specialize le_eq_or_lt x
  10. 0010specialize le_eq_or_lt 2
  11. 0011apply le_eq_or_lt
  12. 0012exact hle2
  13. 0013cases hc2
  14. 0014right
  15. 0015exact hc2_left
  16. 0016left
  17. 0017have hle1 : exists h. h + x = 1
  18. 0018specialize le_of_succ_le_succ x
  19. 0019specialize le_of_succ_le_succ 1
  20. 0020apply le_of_succ_le_succ
  21. 0021exact hc2_right
  22. 0022have hc1 : x = 1 \/ exists h. h + S x = 1
  23. 0023specialize le_eq_or_lt x
  24. 0024specialize le_eq_or_lt 1
  25. 0025apply le_eq_or_lt
  26. 0026exact hle1
  27. 0027cases hc1
  28. 0028right
  29. 0029exact hc1_left
  30. 0030left
  31. 0031have hle0 : exists h. h + x = 0
  32. 0032specialize le_of_succ_le_succ x
  33. 0033specialize le_of_succ_le_succ 0
  34. 0034apply le_of_succ_le_succ
  35. 0035exact hc1_right
  36. 0036specialize le_zero x
  37. 0037apply le_zero
  38. 0038exact hle0