BT0017

le_of_succ_le_succ

Stable · empty-context checked

Successor order reflects to the underlying naturals.

Exact expanded PA statement

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

Structural proof guide

Successor order reflects to the underlying naturals.

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

Proof neighborhood

Direct dependencies

none

Direct dependents

BT002U gcd_exists_up_to BT0034 gcd_balanced_bezout_exists_up_to BT003D factor_property_succ BT003K prime_divisor_exists_up_to BT0059 beta_exclusive_accumulated_product_step BT005A beta_exclusive_recode_congruence_step BT005E beta_prefix_product_trace_exists BT005K beta_product_succ_append BT0069 beta_factor_divides_product BT007V beta_repeat_succ_extend BT0085 beta_range_succ_extend BT0089 beta_prefix_sum_trace_exists BT0097 lt_three_cases BT00AA finite_lt_succ_eq_or_lt BT00JD eisenstein_initial_segment_bit_count_functional BT00PS bounded_prime_interval_search BT00Q5 bounded_power_valuation_search BT00TF beta_pascal_table_diagonal_boundary BT00TM choose_positive BT00VV primorial_le_four_pow_bounded BT00WW bertrand_hj_base_window_thirty_two_from_total BT00X1 six_block_window_decomposition_above_thirty_two BT011A prime_le_twenty_two_cases

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 x
  6. 0006apply PA2
  7. 0007trans x + S a
  8. 0008symm
  9. 0009apply PA4
  10. 0010exact h_witness