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.