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
∀ h. ∀ k. ∀ x. h = 2 · k ∨ h = 2 · k + 1 → Le(x,k) → Le(2 · x,h)Every purple notation token opens its conservative definition. This reading surface never changes the unchanged intuitionistic kernel or confers checked-use authority.
Definitions used by this theorem
In the theorem statement
In local proof propositions
Exact expanded first-order statement
forall h k x. (((h = 2 * k) \/ (h = 2 * k + 1))) -> (exists qst_le_floor. qst_le_floor + (x) = (k)) -> (exists qst_le_doubled. qst_le_doubled + (2 * x) = (h))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only propositions whose conservative expansion has been checked for exact first-order equivalence are compacted. Every changed line retains its immutable exact replay command.
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.
01Fix variables and assumptionsL1–5
02Establish hscaledL6–11
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply mul le mul left.
- L6
have hscaled : Le(2 · x,2 · k)Definitions: Le(2 · x,2 · k)Original native command in the exact edition - L7
specialize mul_le_mul_left x - L8
specialize mul_le_mul_left k - L9
specialize mul_le_mul_left 2 - L10
apply mul_le_mul_left - L11
exact hfloor
03Separate the logical casesL12–12
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L12
cases hhalf
04Calculate and transport equalitiesL13–13
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L13
rewrite hhalf_left
05Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact hscaled
06Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
cases hscaled
07Construct an explicit witnessL16–16
Supply the displayed value, then prove that it has the required property.
- L16
exists S x1
08Calculate and transport equalitiesL17–17
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L17
trans S (x1 + 2 * x)
09Use earlier factsL18–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
apply add_succ_left
Original defined command ledger · 21 lines
- 0001
intro h - 0002
intro k - 0003
intro x - 0004
intro hhalf - 0005
intro hfloor - 0006
have hscaled : Le(2 · x,2 · k)Exact native replay line
have hscaled : exists gap. gap + 2 * x = 2 * k - 0007
specialize mul_le_mul_left x - 0008
specialize mul_le_mul_left k - 0009
specialize mul_le_mul_left 2 - 0010
apply mul_le_mul_left - 0011
exact hfloor - 0012
cases hhalf - 0013
rewrite hhalf_left - 0014
exact hscaled - 0015
cases hscaled - 0016
exists S x1 - 0017
trans S (x1 + 2 * x) - 0018
apply add_succ_left - 0019
rewrite hscaled_witness - 0020
rewrite hhalf_right - 0021
simp