PA000X

lt_to_le

Stable checked-use theorem · independently closed

A witnessed strict inequality entails the corresponding weak inequality.

Exact expanded PA statement

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

Structural proof guide

Generated structural guide

A witnessed strict inequality entails the corresponding weak inequality.

Use the direct prerequisites add_succ_left as previously established PA formulas.

The proof proceeds by case analysis (1).

Referenced ingredients

PA000E add_succ_left

Proof neighborhood

Direct dependencies

PA000E add_succ_left

Direct dependents

PA001U beta_exclusive_accumulated_product_step PA002G beta_exclusive_recode_congruence_step PA008B prime_mul_index_map_exists_up_to PA008S prime_scaled_inverse_prefix_exists_bounded PA009Q pair_index_left_below_double PA00A6 prime_inverse_prefix_exists_bounded PA00D9 distinct_odd_prime_half_cell_oriented

Formal 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.

  1. 0001intro a
  2. 0002intro b
  3. 0003intro h
  4. 0004cases h
  5. 0005exists S x
  6. 0006trans x + S a
  7. 0007trans S (x + a)
  8. 0008apply add_succ_left
  9. 0009symm
  10. 0010apply PA4
  11. 0011exact h_witness