PA003D

finite_lt_succ_eq_or_lt

Stable checked-use theorem · independently closed

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

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

Read the argument

Proof checkpoints

12 script commands · 2 reading checkpoints · 1 local claims

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.

Named ingredients (2)
le of succ le succle eq or lt
01Fix variables and assumptionsL1–3

Work with arbitrary variables or the premises of the current implication.

  1. L1
    intro n
  2. L2
    intro x
  3. L3
    intro hlt
02Establish hleL4–12

Establish this local claim before using it. It is not an additional assumption. The following proof commands apply le of succ le succ.

  1. L4
    have hle : exists h. h + x = n
  2. L5
    specialize le_of_succ_le_succ x
  3. L6
    specialize le_of_succ_le_succ n
  4. L7
    apply le_of_succ_le_succ
  5. L8
    exact hlt
  6. L9
    specialize le_eq_or_lt x
  7. L10
    specialize le_eq_or_lt n
  8. L11
    apply le_eq_or_lt
  9. L12
    exact hle

Library-wide reading audit

Original exact command ledger · 12 lines
  1. 0001intro n
  2. 0002intro x
  3. 0003intro hlt
  4. 0004have hle : exists h. h + x = n
  5. 0005specialize le_of_succ_le_succ x
  6. 0006specialize le_of_succ_le_succ n
  7. 0007apply le_of_succ_le_succ
  8. 0008exact hlt
  9. 0009specialize le_eq_or_lt x
  10. 0010specialize le_eq_or_lt n
  11. 0011apply le_eq_or_lt
  12. 0012exact hle