PA002O · theorem

le_succ

Stable checked-use theorem · independently closed

A weak inequality remains true after raising its upper bound by one.

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

∀ a. ∀ b. Le(a,b) → Le(a,S b)

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

PD0001 Le

2 occurrences

In local proof propositions

none

0 occurrences

Exact expanded native-PA statement
forall a b. (exists k. k + a = b) -> exists r. r + a = S b

Proof neighborhood

Direct theorem prerequisites

PA000E add_succ_left

Direct theorem dependents

PA002P base_le_beta_modulus PA003Y beta_sum_succ_decompose PA0040 all_bits_prefix_succ PA004A beta_product_succ_decompose PA004D pow_successor_decompose PA004H finite_contains_decidable PA004K beta_prefix_swap_last_from_entries PA004M finite_swap_last_bounded PA004O finite_swap_last_injective PA004P finite_bounded_prefix_without_top PA004Q finite_injective_prefix_succ PA004R finite_last_is_top_from_prefix_surjective PA004S finite_surjective_succ_intro PA004U finite_swap_last_surjective_back PA004W finite_bounded_injective_surjective PA004X finite_fixed_last_prefix_bounded PA0051 beta_product_functional PA0052 beta_product_replace_balance PA0053 beta_product_swap_last_invariant PA0065 factorial_succ_decompose PA006K beta_sum_trace_functional PA0074 gauss_signed_half_prefix_exists PA007D beta_magnitude_predecessor_recode_exists PA007H beta_sign_factor_prefix_drop_last PA007M beta_pointwise_mul_prefix_drop_last PA007Q beta_product_pointwise_scale_mod PA007X beta_product_permutation_invariant PA0081 beta_product_pointwise_coprime PA0092 finite_covers_into_or_omits PA0094 finite_inverse_choice_prefix_exists PA0097 finite_short_cover_impossible PA009K beta_prefix_append_two_exists PA009M beta_prefix_append_two_scaled_orbit_closed PA00A0 beta_adjacent_target_pairs_product_power PA00AE finite_prefix_choose_unused_nonendpoint PA00AT beta_prefix_append_two_orbit_closed PA00B9 beta_adjacent_unit_pairs_product_one PA00BG beta_range_two_product_is_factorial_succ PA00CQ beta_sum_pointwise_mod_three_add PA00CU beta_sum_replace_balance PA00CV beta_sum_swap_last_invariant PA00CX beta_sum_permutation_invariant PA00DD eisenstein_row_indicator_prefix_exists PA00DJ eisenstein_rectangle_row_count_prefix_exists PA00DW beta_all_one_bit_count_exact PA00DX eisenstein_initial_segment_bit_count_functional PA00E9 eisenstein_transposed_column_prefix_exists PA00EE complementary_bit_counts_add_length PA00EI eisenstein_transposed_column_count_prefix_exists PA00EK beta_repeat_sum_exact PA00EP beta_sum_pointwise_add PA00ET eisenstein_row_indicator_prefix_succ_restrict PA00EX eisenstein_successor_row_split_prefix_exists PA00F3 eisenstein_fubini_column_count_prefix_succ_restrict PA00F8 eisenstein_fubini_column_count_prefix_retarget_predecessor

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

9 script commands · 7 reading checkpoints · 0 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 (1)
add succ left
01Fix variables and assumptionsL1–3

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

  1. L1
    intro a
  2. L2
    intro b
  3. L3
    intro h
02Separate the logical casesL4–4

Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.

  1. L4
    cases h
03Construct an explicit witnessL5–5

Supply the displayed value, then prove that it has the required property.

  1. L5
    exists S x
04Calculate and transport equalitiesL6–6

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L6
    trans S (x + a)
05Use earlier factsL7–7

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L7
    apply add_succ_left
06Calculate and transport equalitiesL8–8

Carry out the recorded arithmetic or equality steps; inspect the exact commands for their direction and premises.

  1. L8
    congr
07Use earlier factsL9–9

Instantiate or apply named facts and discharge the corresponding proof obligations.

  1. L9
    exact h_witness

Library-wide reading audit

Original defined command ledger · 9 lines
  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004cases h
  5. 0005exists S x
  6. 0006trans S (x + a)
  7. 0007apply add_succ_left
  8. 0008congr
  9. 0009exact h_witness