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 n. ~(n = 0) -> exists k. n = S kStructural proof guide
Generated structural guide
Every nonzero natural has a predecessor.
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by structural induction (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct 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_thresholdFormal native tactic body
Dependencies are introduced as named hypotheses before line 1. Linked names are exact direct references. This Stable checked-use theorem is independently kernel-checked when replayed.
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