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
∀ p. ∀ a. ¬p = 0 → ¬Dvd(p,a) → ∃ x. ¬x = 0 ∧ (Lt(x,p) ∧ ModEq(p,a,x))Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.
Definitions used by this theorem
In the theorem statement
3 occurrences
In local proof propositions
2 occurrences
Exact expanded native-PA statement
forall p a. ~(p = 0) -> (~(exists frm_factor_eca_canonical_not_divisor. a = p * frm_factor_eca_canonical_not_divisor)) -> (exists r. ~(r = 0) /\ ((exists wpo_gap_eca_canonical_bound. wpo_gap_eca_canonical_bound + S (r) = p) /\ (exists wpp_mod_left_eca_canonical_mod wpp_mod_right_eca_canonical_mod. (a) + p * wpp_mod_left_eca_canonical_mod = (r) + p * wpp_mod_right_eca_canonical_mod)))Proof neighborhood
Direct theorem prerequisites
Direct theorem dependents
Definition-aware tactic body
Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed 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.
Named ingredients (3)
01Fix variables and assumptionsL1–4
02Establish hdivisionL5–9
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply division remainder exists.
- L5
have hdivision : ∃ q. ∃ r. DivRem(a,p,q,r)Definitions: DivRem(a,p,q,r)Original native command in the exact edition - L6
specialize division_remainder_exists p - L7
specialize division_remainder_exists a - L8
apply division_remainder_exists - L9
exact hp0
03Separate the logical casesL10–12
04Establish hr0L13–15
05Construct an explicit witnessL16–16
Supply the displayed value, then prove that it has the required property.
- L16
exists x
06Calculate and transport equalitiesL17–17
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L17
trans p * x + x1
07Use earlier factsL18–18
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L18
exact hdivision_witness_witness_left
08Calculate and transport equalitiesL19–20
09Establish hdecompositionL21–26
10Establish hmodL27–33
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply remainder decomposition to mod eq.
11Construct an explicit witnessL34–34
Supply the displayed value, then prove that it has the required property.
- L34
exists x1
12Separate the logical casesL35–35
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L35
split
13Use earlier factsL36–36
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L36
exact hr0
14Separate the logical casesL37–37
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L37
split
Original defined command ledger · 39 lines
- 0001
intro p - 0002
intro a - 0003
intro hp0 - 0004
intro hnotdiv - 0005
have hdivision : ∃ q. ∃ r. DivRem(a,p,q,r)Exact native replay line
have hdivision : exists q r. a = p * q + r /\ exists gap. gap + S r = p - 0006
specialize division_remainder_exists p - 0007
specialize division_remainder_exists a - 0008
apply division_remainder_exists - 0009
exact hp0 - 0010
cases hdivision - 0011
cases hdivision_witness - 0012
cases hdivision_witness_witness - 0013
have hr0 : ~(x1 = 0) - 0014
intro hrzero - 0015
apply hnotdiv - 0016
exists x - 0017
trans p * x + x1 - 0018
exact hdivision_witness_witness_left - 0019
rewrite hrzero - 0020
simp - 0021
have hdecomposition : a = x * p + x1 - 0022
trans p * x + x1 - 0023
exact hdivision_witness_witness_left - 0024
congr - 0025
apply mul_comm - 0026
refl - 0027
have hmod : ModEq(p,a,x1)Exact native replay line
have hmod : exists wpp_mod_left_eca_canonical_proof_mod wpp_mod_right_eca_canonical_proof_mod. (a) + p * wpp_mod_left_eca_canonical_proof_mod = (x1) + p * wpp_mod_right_eca_canonical_proof_mod - 0028
specialize remainder_decomposition_to_mod_eq p - 0029
specialize remainder_decomposition_to_mod_eq a - 0030
specialize remainder_decomposition_to_mod_eq x - 0031
specialize remainder_decomposition_to_mod_eq x1 - 0032
apply remainder_decomposition_to_mod_eq - 0033
exact hdecomposition - 0034
exists x1 - 0035
split - 0036
exact hr0 - 0037
split - 0038
exact hdivision_witness_witness_right - 0039
exact hmod