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
∀ x. Lt(x,3) → x = 0 ∨ x = 1 ∨ x = 2Every 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
1 occurrences
In local proof propositions
5 occurrences
Exact expanded native-PA statement
forall x. (exists h. h + S x = 3) -> x = 0 \/ x = 1 \/ x = 2Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
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
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)
01Fix variables and assumptionsL1–2
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.
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.
04Separate the logical casesL13–14
05Use earlier factsL15–15
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L15
exact hc2_left
06Separate the logical casesL16–16
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- 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.
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.
09Separate the logical casesL27–28
10Use earlier factsL29–29
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L29
exact hc1_left
11Separate the logical casesL30–30
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- 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.
Original defined command ledger · 38 lines
- 0001
intro x - 0002
intro hb - 0003
have hle2 : Le(x,2)Exact native replay line
have hle2 : exists h. h + x = 2 - 0004
specialize le_of_succ_le_succ x - 0005
specialize le_of_succ_le_succ 2 - 0006
apply le_of_succ_le_succ - 0007
exact hb - 0008
have hc2 : x = 2 ∨ Lt(x,2)Exact native replay line
have hc2 : x = 2 \/ exists h. h + S x = 2 - 0009
specialize le_eq_or_lt x - 0010
specialize le_eq_or_lt 2 - 0011
apply le_eq_or_lt - 0012
exact hle2 - 0013
cases hc2 - 0014
right - 0015
exact hc2_left - 0016
left - 0017
have hle1 : Le(x,1)Exact native replay line
have hle1 : exists h. h + x = 1 - 0018
specialize le_of_succ_le_succ x - 0019
specialize le_of_succ_le_succ 1 - 0020
apply le_of_succ_le_succ - 0021
exact hc2_right - 0022
have hc1 : x = 1 ∨ Lt(x,1)Exact native replay line
have hc1 : x = 1 \/ exists h. h + S x = 1 - 0023
specialize le_eq_or_lt x - 0024
specialize le_eq_or_lt 1 - 0025
apply le_eq_or_lt - 0026
exact hle1 - 0027
cases hc1 - 0028
right - 0029
exact hc1_left - 0030
left - 0031
have hle0 : Le(x,0)Exact native replay line
have hle0 : exists h. h + x = 0 - 0032
specialize le_of_succ_le_succ x - 0033
specialize le_of_succ_le_succ 0 - 0034
apply le_of_succ_le_succ - 0035
exact hc1_right - 0036
specialize le_zero x - 0037
apply le_zero - 0038
exact hle0