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
∀ r. ∀ p. ¬r = 0 → Lt(1,p) → Lt(r,r · p)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
2 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall r p. ~(r = 0) -> (exists bpvl_gap_factor_two. bpvl_gap_factor_two + (2) = (p)) -> (exists bpvl_gap_factor_result. bpvl_gap_factor_result + (S r) = (r * p))Proof 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–4
02Establish hstepL5–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul lt mul succ left nonzero.
- L5
have hstep : Lt(r · 1,r · 2)Definitions: Lt(r · 1,r · 2)Original native command in the exact edition - L6
specialize mul_lt_mul_succ_left_nonzero r - L7
specialize mul_lt_mul_succ_left_nonzero 1 - L8
apply mul_lt_mul_succ_left_nonzero - L9
exact hr - L10
specialize mul_one r - L11
rewrite mul_one at hstep
03Establish hscaledL12–21
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.
- L12
have hscaled : Le(r · 2,r · p)Definitions: Le(r · 2,r · p)Original native command in the exact edition - L13
specialize mul_le_mul_left 2 - L14
specialize mul_le_mul_left p - L15
specialize mul_le_mul_left r - L16
apply mul_le_mul_left - L17
exact hp - L18
specialize le_trans (S r) - L19
specialize le_trans (r * 2) - L20
specialize le_trans (r * p) - L21
apply le_trans
Original defined command ledger · 23 lines
- 0001
intro r - 0002
intro p - 0003
intro hr - 0004
intro hp - 0005
have hstep : Lt(r · 1,r · 2)Exact native replay line
have hstep : exists k. k + S (r * 1) = r * 2 - 0006
specialize mul_lt_mul_succ_left_nonzero r - 0007
specialize mul_lt_mul_succ_left_nonzero 1 - 0008
apply mul_lt_mul_succ_left_nonzero - 0009
exact hr - 0010
specialize mul_one r - 0011
rewrite mul_one at hstep - 0012
have hscaled : Le(r · 2,r · p)Exact native replay line
have hscaled : exists k. k + r * 2 = r * p - 0013
specialize mul_le_mul_left 2 - 0014
specialize mul_le_mul_left p - 0015
specialize mul_le_mul_left r - 0016
apply mul_le_mul_left - 0017
exact hp - 0018
specialize le_trans (S r) - 0019
specialize le_trans (r * 2) - 0020
specialize le_trans (r * p) - 0021
apply le_trans - 0022
exact hstep - 0023
exact hscaled