PA003D · theorem

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.

Statement with defined notation

∀ n. ∀ x. Lt(x,S n) → x = n ∨ Lt(x,n)

Every purple notation token opens its conservative definition. This is a reading surface; the compiler expands the statement before the unchanged kernel checks it.

Definitions used by this theorem

In the theorem statement

PD0002 Lt

2 occurrences

In local proof propositions

PD0001 Le

1 occurrences

Exact expanded native-PA statement
forall n x. (exists h. h + S x = S n) -> x = n \/ exists h. h + S x = n

Proof neighborhood

Direct theorem prerequisites

PA000V le_of_succ_le_succ PA000W le_eq_or_lt

Direct theorem 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

Definition-aware tactic body

Only local propositions introduced by have or suffices are compacted. The untrusted compiler re-expands each one before the original tactic script is replayed; defined notation is never accepted by the kernel. Open the exact replay line beneath every changed command.

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.

Definition notation is shown below. Open the paired exact edition for the original native formulas. Source pairing is not a new equivalence certificate.

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
  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 defined command ledger · 12 lines
  1. 0001intro n
  2. 0002intro x
  3. 0003intro hlt
  4. 0004have hle : Le(x,n)
    Exact native replay linehave 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