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
forall n. ~(n = 0) -> exists k. n = S kEvery 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
0 occurrences
In local proof propositions
0 occurrences
Exact expanded native-PA statement
forall n. ~(n = 0) -> exists k. n = S kProof neighborhood
Direct theorem prerequisites
Direct theorem dependents
PA0026 binary_crt PA003Q coprime_mod_inverse PA005M quadratic_residue_bounded_decidable_nonzero PA0061 prime_is_succ_succ PA007D beta_magnitude_predecessor_recode_exists PA007S beta_magnitude_predecessor_recode_bounded PA007T beta_magnitude_predecessor_recode_reflect PA008A mod_eq_zero_to_dvd_nonzero PA008B prime_mul_index_map_exists_up_to PA009A scaled_inverse_prefix_mate_predecessor PA00A2 prime_two_or_terminal_odd_shape PA00A4 prime_inverse_index_exists PA00AG prime_bounded_square_one_cases PA00B4 finite_bounded_nonendpoint_injective_coverage PA00C3 odd_half_positive_complement_exists PA00DS nonzero_remainder_division_positive_multiple_thresholdDefinition-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.
01Induction on nL1–2
02Separate the logical casesL3–3
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L3
exfalso
03Use earlier factsL4–4
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L4
apply h
04Calculate and transport equalitiesL5–5
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L5
refl
05Fix variables and assumptionsL6–6
Work with arbitrary variables or the premises of the current implication.
- L6
intro h
06Construct an explicit witnessL7–7
Supply the displayed value, then prove that it has the required property.
- L7
exists n
07Calculate and transport equalitiesL8–8
Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.
- L8
refl