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
∀ s. ∀ a. ∀ c. ∀ x. Le(a,s) → Le(c,s) → a = c + x ∨ c = a + x → Le(x,s)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 s a c x. (exists ftcn_bound_bounded_first. ftcn_bound_bounded_first + (a) = (s)) -> (exists ftcn_bound_bounded_second. ftcn_bound_bounded_second + (c) = (s)) -> (((a) = (c) + (x) \/ (c) = (a) + (x))) -> (exists ftcn_bound_bounded_result. ftcn_bound_bounded_result + (x) = (s))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–7
02Separate the logical casesL8–9
03Construct an explicit witnessL10–10
Supply the displayed value, then prove that it has the required property.
- L10
exists x1 + c
04Calculate and transport equalitiesL11–11
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L11
trans x1 + (c + x)
05Use earlier factsL12–12
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L12
apply add_assoc
06Calculate and transport equalitiesL13–13
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L13
rewrite <- hdifference_left
07Use earlier factsL14–14
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L14
exact ha_witness
08Separate the logical casesL15–15
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L15
cases hc
09Construct an explicit witnessL16–16
Supply the displayed value, then prove that it has the required property.
- L16
exists x1 + a
10Calculate and transport equalitiesL17–17
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L17
trans x1 + (a + x)
11Use earlier factsL18–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
apply add_assoc
12Calculate and transport equalitiesL19–19
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L19
rewrite <- hdifference_right
13Use earlier factsL20–20
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L20
exact hc_witness
Original defined command ledger · 20 lines
- 0001
intro s - 0002
intro a - 0003
intro c - 0004
intro x - 0005
intro ha - 0006
intro hc - 0007
intro hdifference - 0008
cases hdifference - 0009
cases ha - 0010
exists x1 + c - 0011
trans x1 + (c + x) - 0012
apply add_assoc - 0013
rewrite <- hdifference_left - 0014
exact ha_witness - 0015
cases hc - 0016
exists x1 + a - 0017
trans x1 + (a + x) - 0018
apply add_assoc - 0019
rewrite <- hdifference_right - 0020
exact hc_witness