BT0018

le_succ

Stable · empty-context checked

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

Exact expanded PA statement

forall a b. (exists k. k + a = b) -> exists r. r + a = S b

Structural proof guide

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

Direct prerequisites: add_succ_left. The authored body proceeds by case analysis (1).

Proof neighborhood

Direct dependencies

BT0001 add_succ_left

Direct dependents

BT003E factor_search_up_to BT0054 base_le_beta_modulus BT005G beta_product_functional BT005J beta_product_succ_decompose BT0083 pow_successor_decompose BT008B beta_sum_trace_functional BT008F beta_sum_succ_decompose BT008J all_bits_prefix_succ BT0092 factorial_succ_decompose BT00DH beta_product_pointwise_coprime BT00JC beta_all_one_bit_count_exact BT00JD eisenstein_initial_segment_bit_count_functional BT00K5 beta_sum_pointwise_add BT00PS bounded_prime_interval_search BT00Q5 bounded_power_valuation_search BT00RA floor_sqrt_total BT00ST legendre_sum_zero_extended_prefix BT00TI choose_succ_succ_of_lt BT00TJ choose_succ_succ BT00UD primorial_succ_decompose BT00UQ beta_product_prefix_suffix_split BT00VB factorial_prime_le_of_divides BT00VD beta_pairwise_coprime_product_divides_common_multiple BT00X9 beta_product_pointwise_le BT00XQ power_quotient_prefix_sum_extend_zero BT00XX double_quotient_carry_prefix_exists BT00Y0 double_quotient_carry_prefix_restrict BT00Y1 bit_count_positive_last_one BT010B floor_sqrt_two_le_of_two_lt BT010U beta_product_all_one_exact

Formal native tactic body

Dependencies are hypotheses of this body receipt. The focused endpoint audits separately check the complete empty-context certificates.

  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