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.
Exact expanded PA statement
forall p a. ~(a = 0) -> (exists wpo_gap_ecb_a_lt_p. wpo_gap_ecb_a_lt_p + S (a) = p) -> (~(exists frm_factor_ecb_not_divisor. a = p * frm_factor_ecb_not_divisor))Structural proof guide
Generated structural guide
A nonzero value strictly below a modulus is not divisible by it.
Use the direct prerequisites divisor_le_nonzero, lt_not_le as previously established PA formulas.
The proof proceeds by intermediate claims (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct dependents
Formal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Alpha-v25 checked-use theorem is independently kernel-checked when replayed; it is not a Stable theorem.
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 (2)
01Fix variables and assumptionsL1–5
02Establish hpaL6–15
Establish this local claim before using it. It is not an additional assumption. The following proof commands apply divisor le nonzero.
03Use earlier factsL16–16
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L16
exact hpa
Original exact command ledger · 16 lines
- 0001
intro p - 0002
intro a - 0003
intro ha0 - 0004
intro hap - 0005
intro hdiv - 0006
have hpa : exists t. t + p = a - 0007
specialize divisor_le_nonzero p - 0008
specialize divisor_le_nonzero a - 0009
apply divisor_le_nonzero - 0010
exact ha0 - 0011
exact hdiv - 0012
specialize lt_not_le a - 0013
specialize lt_not_le p - 0014
apply lt_not_le - 0015
exact hap - 0016
exact hpa