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 a b. (exists k. k + a = b) -> exists r. r + a = S bStructural proof guide
Generated structural guide
A weak inequality remains true after raising its upper bound by one.
Use the direct prerequisites add_succ_left as previously established PA formulas.
The proof proceeds by case analysis (1).
Referenced ingredients
Proof neighborhood
Direct dependencies
Direct 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_predecessorFormal 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
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 (1)
01Fix variables and assumptionsL1–3
02Separate the logical casesL4–4
Follow the explicit conjunction, disjunction, witness, or contradiction step recorded below.
- L4
cases h
03Construct an explicit witnessL5–5
Supply the displayed value, then prove that it has the required property.
- 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.
- L6
trans S (x + a)
05Use earlier factsL7–7
Instantiate or apply named facts and discharge the corresponding proof obligations.
- 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.
- L8
congr
07Use earlier factsL9–9
Instantiate or apply named facts and discharge the corresponding proof obligations.
- L9
exact h_witness