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
∀ n. ∀ c. ∀ d. ¬n = 0 → n = c · d → ¬d = 1 → Lt(c,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
1 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall n c d. ~(n = 0) -> n = c * d -> ~(d = 1) -> exists k. k + S c = nProof 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 (4)
01Fix variables and assumptionsL1–6
02Establish hleL7–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor le nonzero.
03Construct an explicit witnessL12–12
Supply the displayed value, then prove that it has the required property.
- L12
exists d
04Use earlier factsL13–13
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L13
exact hfactor
05Establish hcasesL14–18
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le eq or lt.
06Separate the logical casesL19–20
07Use earlier factsL21–21
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L21
apply hd
08Establish hcL22–31
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply hn.
09Use earlier factsL32–33
10Calculate and transport equalitiesL34–35
11Use earlier factsL36–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
exact hfactor
12Calculate and transport equalitiesL37–38
13Use earlier factsL39–39
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L39
exact hcases_left
14Calculate and transport equalitiesL40–40
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L40
symm
Original defined command ledger · 43 lines
- 0001
intro n - 0002
intro c - 0003
intro d - 0004
intro hn - 0005
intro hfactor - 0006
intro hd - 0007
have hle : Le(c,n)Exact native replay line
have hle : exists k. k + c = n - 0008
specialize divisor_le_nonzero c - 0009
specialize divisor_le_nonzero n - 0010
apply divisor_le_nonzero - 0011
exact hn - 0012
exists d - 0013
exact hfactor - 0014
have hcases : c = n ∨ Lt(c,n)Exact native replay line
have hcases : c = n \/ exists k. k + S c = n - 0015
specialize le_eq_or_lt c - 0016
specialize le_eq_or_lt n - 0017
apply le_eq_or_lt - 0018
exact hle - 0019
cases hcases - 0020
exfalso - 0021
apply hd - 0022
have hc : ~(c = 0) - 0023
intro hc0 - 0024
apply hn - 0025
trans c - 0026
symm - 0027
exact hcases_left - 0028
exact hc0 - 0029
specialize mul_left_cancel_nonzero c - 0030
specialize mul_left_cancel_nonzero d - 0031
specialize mul_left_cancel_nonzero 1 - 0032
apply mul_left_cancel_nonzero - 0033
exact hc - 0034
trans n - 0035
symm - 0036
exact hfactor - 0037
trans c - 0038
symm - 0039
exact hcases_left - 0040
symm - 0041
specialize mul_one c - 0042
exact mul_one - 0043
exact hcases_right