PA001V

nonzero_is_succ

Stable checked-use theorem · independently closed

Every nonzero natural has a predecessor.

Exact expanded PA statement

forall n. ~(n = 0) -> exists k. n = S k

Structural 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

none

Proof neighborhood

Direct dependencies

none

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_threshold

Formal 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.

  1. 0001induction n
  2. 0002intro h
  3. 0003exfalso
  4. 0004apply h
  5. 0005refl
  6. 0006intro h
  7. 0007exists n
  8. 0008refl