PA003D — finite_lt_succ_eq_or

Exact expanded PA statement

forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n

Structural proof guide

Generated structural guide

A value below a successor is the predecessor or lies below it.

Use the direct prerequisites le_of_succ_le_succ, le_eq_or_lt as previously established PA formulas.

The proof proceeds by intermediate claims (1).

Referenced ingredients

PA000V le_of_succ_le_succ PA000W le_eq_or_lt

Proof neighborhood

Direct dependencies

PA000V le_of_succ_le_succ PA000W le_eq_or_lt

Direct dependents

PA004H finite_contains_decidable PA004J beta_prefix_replace_exists PA004P finite_bounded_prefix_without_top PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro PA0052 beta_product_replace_balance PA0073 gauss_signed_half_prefix_extend PA007D beta_magnitude_predecessor_recode_exists PA007F beta_sign_factor_prefix_extend PA007K beta_pointwise_mul_prefix_extend PA007X beta_product_permutation_invariant PA008B prime_mul_index_map_exists_up_to PA008C beta_successor_lift_exists PA008R prime_scaled_inverse_prefix_extend PA0092 finite_covers_into_or_omits PA0093 finite_inverse_choice_prefix_extend PA009L beta_prefix_append_two_reflect PA009P beta_prefix_append_two_bounded_into PA009S adjacent_scaled_orbit_history_append PA00A5 prime_inverse_prefix_extend PA00AY paired_inverse_witness_append PA00BX beta_division_prefix_extend PA00CU beta_sum_replace_balance PA00CX beta_sum_permutation_invariant PA00DC eisenstein_row_indicator_prefix_extend PA00DI eisenstein_rectangle_row_count_prefix_extend PA00E8 eisenstein_transposed_column_prefix_extend PA00EH eisenstein_transposed_column_count_prefix_extend PA00EW eisenstein_successor_row_split_prefix_extend

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.