Exact expanded PA statement
forall n. ~(S n = 0)Structural proof guide
Generated structural guide
No successor is zero (the reusable PA1 lemma).
This root lemma is proved directly from the PA rules and the hypotheses introduced by its statement.
The proof proceeds by direct introduction and elimination.
Referenced ingredients
none
Proof neighborhood
Direct dependencies
none
Direct dependents
PA0006 beta_range_empty PA000I bounded_common_multiple_step PA000K bounded_common_multiple_exists PA000U beta_modulus_nonzero PA002I bounded_beta_exclusive_recode_invariant PA0031 prime_nonzero PA003G beta_prefix_sum_trace_exists PA003W beta_prefix_product_trace_exists PA0043 beta_repeat_empty PA004F finite_surjective_zero PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA0052 beta_product_replace_balance PA0063 prime_bounded_nonzero_mod_inverse PA006S mul_left_cancel_nonzero PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007G beta_sign_factor_prefix_exists PA007L beta_pointwise_mul_prefix_exists PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008K prime_range_product_coprime PA008R prime_scaled_inverse_prefix_extend PA008S prime_scaled_inverse_prefix_exists_bounded PA008U scaled_orbit_closed_prefix_zero PA008V bounded_into_zero PA008W injective_prefix_zero PA008Y adjacent_scaled_orbit_history_zero PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA00A4 prime_inverse_index_exists PA00A6 prime_inverse_prefix_exists_bounded PA00A8 orbit_closed_prefix_zero PA00A9 nonendpoint_prefix_zero PA00AB paired_inverse_witness_zero PA00AG prime_bounded_square_one_cases PA00BY beta_division_prefix_exists PA00CU beta_sum_replace_balance PA00D8 distinct_odd_prime_half_products_ne PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00DN prime_nondivisor_bounded_scaled_remainder_nonzero PA00E9 eisenstein_transposed_column_prefix_exists PA00EI eisenstein_transposed_column_count_prefix_exists PA00EX eisenstein_successor_row_split_prefix_existsFormal 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.